The bear does not need the mouse. The lion is young. The mouse needs the bear. The squirrel is big. All young things are cold.
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
The lion is young.
("lion" "is" "young" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
The bear does not need the mouse.
True
1
proof
[(triple1)]
("bear" "needs" "mouse" "-")
triple1
The bear needs the mouse.
False
1
inv-proof
[(triple1)]
("bear" "needs" "mouse" "+")
triple1
The lion is cold.
True
2
proof
[(((triple2) -> rule1))]
("lion" "is" "cold" "+")
((triple2) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not cold.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "is" "cold" "-")
((triple2) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The bear is not cold.
Unknown
inv-rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "cold" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "cold" "+")
The lion does not chase the mouse.
Unknown
inv-random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The bear does not need the mouse.[(triple1)] The lion is young.[(triple2)] The mouse needs the bear.[(triple3)] The squirrel is big.[(triple4)] @1: The lion is cold.[(((triple2) -> rule1))]
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple3
The squirrel is big.
("squirrel" "is" "big" "+")
triple4
The lion is cold.
("lion" "is" "cold" "+")
((triple2) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1