The lion eats the mouse. The mouse visits the squirrel. The squirrel eats the lion. If something eats the lion then it is cold.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
If something eats the lion then it is cold.
((("something" "eats" "lion" "+")) -> ("something" "is" "cold" "+"))
The mouse visits the squirrel.
True
1
proof
[(triple2)]
("mouse" "visits" "squirrel" "+")
triple2
The lion does not eat the mouse.
False
1
inv-proof
[(triple1)]
("lion" "eats" "mouse" "-")
triple1
The squirrel is cold.
True
2
proof
[(((triple3) -> rule1))]
("squirrel" "is" "cold" "+")
((triple3) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is not cold.
False
2
inv-proof
[(((triple3) -> rule1))]
("squirrel" "is" "cold" "-")
((triple3) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "cold" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "cold" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The squirrel visits the lion.
Unknown
random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "+")
@0: The lion eats the mouse.[(triple1)] The mouse visits the squirrel.[(triple2)] The squirrel eats the lion.[(triple3)] @1: The squirrel is cold.[(((triple3) -> rule1))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple3
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple3) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1