The mouse is kind. The mouse is rough. The mouse likes the squirrel. The mouse needs the squirrel. The mouse needs the tiger. The mouse sees the squirrel. The squirrel is cold. The squirrel is rough. The squirrel does not like the mouse. The squirrel does not like the tiger. The squirrel needs the tiger. The tiger is nice. The tiger is not rough. The tiger needs the squirrel. The tiger does not see the mouse. If someone sees the tiger then the tiger is kind. If someone is rough then they need the mouse. If someone likes the squirrel and the squirrel likes the mouse then they are young. If someone needs the mouse then the mouse sees the tiger. If someone sees the squirrel and they are rough then they need the tiger. If the tiger likes the squirrel then the squirrel likes the mouse. If someone likes the squirrel then the squirrel sees the mouse. If someone is kind then they like the tiger.
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
The squirrel does not like the tiger.
("squirrel" "likes" "tiger" "-")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger does not see the mouse.
("tiger" "sees" "mouse" "-")
If someone sees the tiger then the tiger is kind.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If someone is rough then they need the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "mouse" "+"))
If someone likes the squirrel and the squirrel likes the mouse then they are young.
((("someone" "likes" "squirrel" "+") ("squirrel" "likes" "mouse" "+")) -> ("someone" "is" "young" "+"))
If someone needs the mouse then the mouse sees the tiger.
((("someone" "needs" "mouse" "+")) -> ("mouse" "sees" "tiger" "+"))
If someone sees the squirrel and they are rough then they need the tiger.
((("someone" "sees" "squirrel" "+") ("someone" "is" "rough" "+")) -> ("someone" "needs" "tiger" "+"))
If the tiger likes the squirrel then the squirrel likes the mouse.
((("tiger" "likes" "squirrel" "+")) -> ("squirrel" "likes" "mouse" "+"))
If someone likes the squirrel then the squirrel sees the mouse.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "sees" "mouse" "+"))
If someone is kind then they like the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "tiger" "+"))
The mouse sees the squirrel.
True
1
proof
[(triple6)]
("mouse" "sees" "squirrel" "+")
triple6
The squirrel does not need the tiger.
False
1
inv-proof
[(triple11)]
("squirrel" "needs" "tiger" "-")
triple11
The squirrel sees the mouse.
True
2
proof
[(((triple3) -> rule7))]
("squirrel" "sees" "mouse" "+")
((triple3) -> (rule7 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The mouse does not need the mouse.
False
2
inv-proof
[(((triple2) -> rule2))]
("mouse" "needs" "mouse" "-")
((triple2) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the tiger.
True
3
proof
[(((((triple2) -> rule2)) -> rule4) OR ((((triple8) -> rule2)) -> rule4))]
("mouse" "sees" "tiger" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The mouse does not see the tiger.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4) OR ((((triple8) -> rule2)) -> rule4))]
("mouse" "sees" "tiger" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The tiger is kind.
True
4
proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule1) OR ((((((triple8) -> rule2)) -> rule4)) -> rule1))]
("tiger" "is" "kind" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The tiger is not kind.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule1) OR ((((((triple8) -> rule2)) -> rule4)) -> rule1))]
("tiger" "is" "kind" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "young" "-")
The tiger needs the tiger.
Unknown
rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "young" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "young" "+")
The tiger does not see the squirrel.
Unknown
inv-random
[@0: The tiger sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "squirrel" "-")
The tiger likes the mouse.
Unknown
random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "+")
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The mouse is kind.[(triple1)] The mouse is rough.[(triple2)] The mouse likes the squirrel.[(triple3)] The mouse needs the squirrel.[(triple4)] The mouse needs the tiger.[(triple5 OR ((triple6 triple2) -> rule5))] The mouse sees the squirrel.[(triple6)] The squirrel does not like the mouse.[(triple9)] The squirrel does not like the tiger.[(triple10)] The squirrel is cold.[(triple7)] The squirrel is rough.[(triple8)] The squirrel needs the tiger.[(triple11)] The tiger does not see the mouse.[(triple15)] The tiger is nice.[(triple12)] The tiger is not rough.[(triple13)] The tiger needs the squirrel.[(triple14)] @1: The mouse likes the tiger.[(((triple1) -> rule8))] The mouse needs the mouse.[(((triple2) -> rule2))] The squirrel needs the mouse.[(((triple8) -> rule2))] The squirrel sees the mouse.[(((triple3) -> rule7))] @2: The mouse sees the tiger.[(((((triple2) -> rule2)) -> rule4) OR ((((triple8) -> rule2)) -> rule4))] @3: The tiger is kind.[(((((((triple2) -> rule2)) -> rule4)) -> rule1) OR ((((((triple8) -> rule2)) -> rule4)) -> rule1))] @4: The tiger likes the tiger.[(((((((((triple2) -> rule2)) -> rule4)) -> rule1)) -> rule8) OR ((((((((triple8) -> rule2)) -> rule4)) -> rule1)) -> rule8))]
The mouse is kind.
("mouse" "is" "kind" "+")
triple1
The mouse is rough.
("mouse" "is" "rough" "+")
triple2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple3
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple4
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple5
((triple6 triple2) -> (rule5 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple6
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
triple9
The squirrel does not like the tiger.
("squirrel" "likes" "tiger" "-")
triple10
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple7
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple8
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple11
The tiger does not see the mouse.
("tiger" "sees" "mouse" "-")
triple15
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger is not rough.
("tiger" "is" "rough" "-")
triple13
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple14
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((triple1) -> (rule8 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple2) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
((triple8) -> (rule2 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((triple3) -> (rule7 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int4
((((((((triple8) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int4