The cow is kind. The mouse eats the cow. The mouse eats the squirrel. The mouse is green. The mouse sees the squirrel. The squirrel eats the mouse. The squirrel is big. The squirrel is young. The squirrel likes the tiger. The tiger sees the cow. If someone is big then they eat the squirrel. If someone likes the mouse then the mouse eats the squirrel. If someone is green then they see the tiger. If someone eats the squirrel and the squirrel is young then the squirrel likes the cow. If the tiger eats the mouse and the tiger sees the squirrel then the squirrel likes the mouse. If someone is kind then they are green. If the tiger is blue then the tiger is green. If someone sees the tiger then they see the mouse.
The cow is kind.
("cow" "is" "kind" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If someone is big then they eat the squirrel.
((("someone" "is" "big" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone likes the mouse then the mouse eats the squirrel.
((("someone" "likes" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
If someone is green then they see the tiger.
((("someone" "is" "green" "+")) -> ("someone" "sees" "tiger" "+"))
If someone eats the squirrel and the squirrel is young then the squirrel likes the cow.
((("someone" "eats" "squirrel" "+") ("squirrel" "is" "young" "+")) -> ("squirrel" "likes" "cow" "+"))
If the tiger eats the mouse and the tiger sees the squirrel then the squirrel likes the mouse.
((("tiger" "eats" "mouse" "+") ("tiger" "sees" "squirrel" "+")) -> ("squirrel" "likes" "mouse" "+"))
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If the tiger is blue then the tiger is green.
((("tiger" "is" "blue" "+")) -> ("tiger" "is" "green" "+"))
If someone sees the tiger then they see the mouse.
((("someone" "sees" "tiger" "+")) -> ("someone" "sees" "mouse" "+"))
The squirrel eats the mouse.
True
1
proof
[(triple6)]
("squirrel" "eats" "mouse" "+")
triple6
The mouse is not green.
False
1
inv-proof
[(triple4)]
("mouse" "is" "green" "-")
triple4
The cow is green.
True
2
proof
[(((triple1) -> rule6))]
("cow" "is" "green" "+")
((triple1) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not green.
False
2
inv-proof
[(((triple1) -> rule6))]
("cow" "is" "green" "-")
((triple1) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The mouse sees the mouse.
True
3
proof
[(((((triple4) -> rule3)) -> rule8))]
("mouse" "sees" "mouse" "+")
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse does not see the mouse.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule8))]
("mouse" "sees" "mouse" "-")
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The cow sees the mouse.
True
4
proof
[(((((((triple1) -> rule6)) -> rule3)) -> rule8))]
("cow" "sees" "mouse" "+")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow does not see the mouse.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule3)) -> rule8))]
("cow" "sees" "mouse" "-")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The squirrel is not green.
Unknown
inv-rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "green" "-")
The tiger is green.
Unknown
rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "green" "+")
The squirrel does not see the mouse.
Unknown
inv-rconc
[@3: The squirrel sees the mouse.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule6 <- FAIL)]]
("squirrel" "sees" "mouse" "-")
The tiger sees the mouse.
Unknown
rconc
[@3: The tiger sees the mouse.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule6 <- FAIL)]]
("tiger" "sees" "mouse" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The mouse likes the tiger.
Unknown
random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "+")
The cow does not like the tiger.
Unknown
inv-random
[@0: The cow likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "tiger" "-")
The cow likes the mouse.
Unknown
random
[@0: The cow likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "mouse" "+")
@0: The cow is kind.[(triple1)] The mouse eats the cow.[(triple2)] The mouse eats the squirrel.[(triple3)] The mouse is green.[(triple4)] The mouse sees the squirrel.[(triple5)] The squirrel eats the mouse.[(triple6)] The squirrel is big.[(triple7)] The squirrel is young.[(triple8)] The squirrel likes the tiger.[(triple9)] The tiger sees the cow.[(triple10)] @1: The cow is green.[(((triple1) -> rule6))] The mouse sees the tiger.[(((triple4) -> rule3))] The squirrel eats the squirrel.[(((triple7) -> rule1))] The squirrel likes the cow.[(((triple3 triple8) -> rule4) OR ((((triple7) -> rule1) triple8) -> rule4))] @2: The cow sees the tiger.[(((((triple1) -> rule6)) -> rule3))] The mouse sees the mouse.[(((((triple4) -> rule3)) -> rule8))] @3: The cow sees the mouse.[(((((((triple1) -> rule6)) -> rule3)) -> rule8))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple3
The mouse is green.
("mouse" "is" "green" "+")
triple4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple5
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple7
The squirrel is young.
("squirrel" "is" "young" "+")
triple8
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple9
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple10
The cow is green.
("cow" "is" "green" "+")
((triple1) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((triple4) -> (rule3 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple7) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
((triple3 triple8) -> (rule4 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
((((triple7) -> (rule1 % int2)) triple8) -> (rule4 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3