The lion is kind. The mouse does not need the squirrel. The squirrel needs the mouse. The tiger is green. If someone chases the squirrel then the squirrel is young. If someone is young and they do not need the squirrel then they are kind. Young people are cold. If someone is round and they see the squirrel then they see the mouse. If someone is young then they see the mouse. If someone is green and they do not chase the lion then they see the lion. If someone sees the squirrel then they are round. If someone needs the mouse then they are young.
The lion is kind.
("lion" "is" "kind" "+")
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The tiger is green.
("tiger" "is" "green" "+")
If someone chases the squirrel then the squirrel is young.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "is" "young" "+"))
If someone is young and they do not need the squirrel then they are kind.
((("someone" "is" "young" "+") ("someone" "needs" "squirrel" "~")) -> ("someone" "is" "kind" "+"))
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is round and they see the squirrel then they see the mouse.
((("someone" "is" "round" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is young then they see the mouse.
((("someone" "is" "young" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is green and they do not chase the lion then they see the lion.
((("someone" "is" "green" "+") ("someone" "chases" "lion" "~")) -> ("someone" "sees" "lion" "+"))
If someone sees the squirrel then they are round.
((("someone" "sees" "squirrel" "+")) -> ("someone" "is" "round" "+"))
If someone needs the mouse then they are young.
((("someone" "needs" "mouse" "+")) -> ("someone" "is" "young" "+"))
The squirrel needs the mouse.
True
1
proof
[(triple3)]
("squirrel" "needs" "mouse" "+")
triple3
The mouse needs the squirrel.
False
1
inv-proof
[(triple2)]
("mouse" "needs" "squirrel" "+")
triple2
The squirrel is young.
True
2
proof
[(((triple3) -> rule8))]
("squirrel" "is" "young" "+")
((triple3) -> (rule8 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is not young.
False
2
inv-proof
[(((triple3) -> rule8))]
("squirrel" "is" "young" "-")
((triple3) -> (rule8 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
True
3
proof
[(((((triple3) -> rule8)) -> rule3))]
("squirrel" "is" "cold" "+")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel does not see the mouse.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule5))]
("squirrel" "sees" "mouse" "-")
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The tiger does not see the lion.
Unknown
inv-rconc
[@1: The tiger sees the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "lion" "-")
The lion is cold.
Unknown
rconc
[@2: The lion is cold.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("lion" "is" "cold" "+")
The squirrel is not kind.
Unknown
inv-rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel chases the tiger.
Unknown
random
[@0: The squirrel chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "tiger" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The lion is kind.[(triple1)] The mouse does not need the squirrel.[(triple2)] The squirrel needs the mouse.[(triple3)] The tiger is green.[(triple4)] @1: The squirrel is young.[(((triple3) -> rule8))] @2: The squirrel is cold.[(((((triple3) -> rule8)) -> rule3))] The squirrel sees the mouse.[(((((triple3) -> rule8)) -> rule5))]
The lion is kind.
("lion" "is" "kind" "+")
triple1
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
triple2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple3
The tiger is green.
("tiger" "is" "green" "+")
triple4
The squirrel is young.
("squirrel" "is" "young" "+")
((triple3) -> (rule8 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2