The lion is blue. The lion is rough. The lion needs the mouse. The lion sees the mouse. The lion does not visit the mouse. The mouse is not green. The mouse needs the lion. The mouse sees the lion. The mouse visits the lion. The squirrel needs the mouse. The squirrel sees the mouse. The squirrel visits the lion. If someone visits the lion then the lion is not young. If someone needs the mouse and they are not young then the mouse sees the squirrel. If someone needs the squirrel and they are rough then the squirrel is cold. If someone is cold then they need the mouse. If someone sees the squirrel then the squirrel is rough. If someone needs the mouse then they are green.
The lion is blue.
("lion" "is" "blue" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If someone visits the lion then the lion is not young.
((("someone" "visits" "lion" "+")) -> ("lion" "is" "young" "-"))
If someone needs the mouse and they are not young then the mouse sees the squirrel.
((("someone" "needs" "mouse" "+") ("someone" "is" "young" "~")) -> ("mouse" "sees" "squirrel" "+"))
If someone needs the squirrel and they are rough then the squirrel is cold.
((("someone" "needs" "squirrel" "+") ("someone" "is" "rough" "+")) -> ("squirrel" "is" "cold" "+"))
If someone is cold then they need the mouse.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "mouse" "+"))
If someone sees the squirrel then the squirrel is rough.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
If someone needs the mouse then they are green.
((("someone" "needs" "mouse" "+")) -> ("someone" "is" "green" "+"))
The squirrel needs the mouse.
True
1
proof
[(triple10)]
("squirrel" "needs" "mouse" "+")
triple10
The lion does not see the mouse.
False
1
inv-proof
[(triple4)]
("lion" "sees" "mouse" "-")
triple4
The squirrel is green.
True
2
proof
[(((triple10) -> rule6))]
("squirrel" "is" "green" "+")
((triple10) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The lion is not green.
False
2
inv-proof
[(((triple3) -> rule6))]
("lion" "is" "green" "-")
((triple3) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The mouse sees the squirrel.
True
4
proof
[(((triple3 ((triple12) -> rule1)) -> rule2) OR ((triple3 ((triple9) -> rule1)) -> rule2))]
("mouse" "sees" "squirrel" "+")
((triple3 ((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The lion is not young.
("lion" "is" "young" "-")
int2
((triple3 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The lion is not young.
("lion" "is" "young" "-")
int2
The mouse does not see the squirrel.
False
4
inv-proof
[(((triple3 ((triple12) -> rule1)) -> rule2) OR ((triple3 ((triple9) -> rule1)) -> rule2))]
("mouse" "sees" "squirrel" "-")
((triple3 ((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The lion is not young.
("lion" "is" "young" "-")
int2
((triple3 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The lion is not young.
("lion" "is" "young" "-")
int2
The squirrel is rough.
True
5
proof
[(((((triple3 ((triple12) -> rule1)) -> rule2)) -> rule5) OR ((((triple3 ((triple9) -> rule1)) -> rule2)) -> rule5))]
("squirrel" "is" "rough" "+")
((((triple3 ((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The lion is not young.
("lion" "is" "young" "-")
int3
((((triple3 ((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The lion is not young.
("lion" "is" "young" "-")
int3
The squirrel is not rough.
False
5
inv-proof
[(((((triple3 ((triple12) -> rule1)) -> rule2)) -> rule5) OR ((((triple3 ((triple9) -> rule1)) -> rule2)) -> rule5))]
("squirrel" "is" "rough" "-")
((((triple3 ((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The lion is not young.
("lion" "is" "young" "-")
int3
((((triple3 ((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The lion is not young.
("lion" "is" "young" "-")
int3
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "cold" "+")
The mouse does not need the squirrel.
Unknown
inv-random
[@0: The mouse needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The squirrel does not visit the mouse.
Unknown
inv-random
[@0: The squirrel visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The lion does not visit the mouse.[(triple5)] The lion is blue.[(triple1)] The lion is rough.[(triple2)] The lion needs the mouse.[(triple3)] The lion sees the mouse.[(triple4)] The mouse is not green.[(triple6)] The mouse needs the lion.[(triple7)] The mouse sees the lion.[(triple8)] The mouse visits the lion.[(triple9)] The squirrel needs the mouse.[(triple10)] The squirrel sees the mouse.[(triple11)] The squirrel visits the lion.[(triple12)] @1: The lion is green.[(((triple3) -> rule6))] The lion is not young.[(((triple12) -> rule1) OR ((triple9) -> rule1))] The squirrel is green.[(((triple10) -> rule6))] @2: The mouse sees the squirrel.[(((triple3 ((triple12) -> rule1)) -> rule2) OR ((triple3 ((triple9) -> rule1)) -> rule2))] @3: The squirrel is rough.[(((((triple3 ((triple12) -> rule1)) -> rule2)) -> rule5) OR ((((triple3 ((triple9) -> rule1)) -> rule2)) -> rule5))]
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple3
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple4
The mouse is not green.
("mouse" "is" "green" "-")
triple6
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple7
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple8
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple9
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple10
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple11
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple12
The lion is green.
("lion" "is" "green" "+")
((triple3) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is not young.
("lion" "is" "young" "-")
((triple12) -> (rule1 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
((triple9) -> (rule1 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple10) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple3 ((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The lion is not young.
("lion" "is" "young" "-")
int2
((triple3 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The lion is not young.
("lion" "is" "young" "-")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((triple3 ((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The lion is not young.
("lion" "is" "young" "-")
int3
((((triple3 ((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The lion is not young.
("lion" "is" "young" "-")
int3