The lion chases the squirrel. The lion eats the squirrel. The lion is nice. The lion needs the mouse. The mouse is rough. The squirrel eats the mouse. The tiger is young. If something needs the tiger then the tiger eats the lion. If something is rough and it needs the mouse then it eats the lion. If something needs the squirrel and it is cold then the squirrel needs the lion. If the lion chases the mouse then the mouse is cold. If something needs the tiger then it chases the squirrel. If something chases the tiger then the tiger is cold. If something is young then it eats the mouse. If something needs the lion and it needs the squirrel then it is big.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The tiger is young.
("tiger" "is" "young" "+")
If something needs the tiger then the tiger eats the lion.
((("something" "needs" "tiger" "+")) -> ("tiger" "eats" "lion" "+"))
If something is rough and it needs the mouse then it eats the lion.
((("something" "is" "rough" "+") ("something" "needs" "mouse" "+")) -> ("something" "eats" "lion" "+"))
If something needs the squirrel and it is cold then the squirrel needs the lion.
((("something" "needs" "squirrel" "+") ("something" "is" "cold" "+")) -> ("squirrel" "needs" "lion" "+"))
If the lion chases the mouse then the mouse is cold.
((("lion" "chases" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If something needs the tiger then it chases the squirrel.
((("something" "needs" "tiger" "+")) -> ("something" "chases" "squirrel" "+"))
If something chases the tiger then the tiger is cold.
((("something" "chases" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If something is young then it eats the mouse.
((("something" "is" "young" "+")) -> ("something" "eats" "mouse" "+"))
If something needs the lion and it needs the squirrel then it is big.
((("something" "needs" "lion" "+") ("something" "needs" "squirrel" "+")) -> ("something" "is" "big" "+"))
The lion chases the squirrel.
True
1
proof
[(triple1)]
("lion" "chases" "squirrel" "+")
triple1
The tiger is not young.
False
1
inv-proof
[(triple7)]
("tiger" "is" "young" "-")
triple7
The tiger eats the mouse.
True
2
proof
[(((triple7) -> rule7))]
("tiger" "eats" "mouse" "+")
((triple7) -> (rule7 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger does not eat the mouse.
False
2
inv-proof
[(((triple7) -> rule7))]
("tiger" "eats" "mouse" "-")
((triple7) -> (rule7 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "lion" "-")
The tiger eats the lion.
Unknown
rconc
[@1: The tiger eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "lion" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The tiger needs the squirrel.
Unknown
random
[@0: The tiger needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "squirrel" "+")
@0: The lion chases the squirrel.[(triple1)] The lion eats the squirrel.[(triple2)] The lion is nice.[(triple3)] The lion needs the mouse.[(triple4)] The mouse is rough.[(triple5)] The squirrel eats the mouse.[(triple6)] The tiger is young.[(triple7)] @1: The tiger eats the mouse.[(((triple7) -> rule7))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple6
The tiger is young.
("tiger" "is" "young" "+")
triple7
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((triple7) -> (rule7 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1