The lion is nice. The mouse is green. The squirrel is green. If the mouse is green then the mouse likes the lion. If something is red and it likes the mouse then it eats the mouse. If something visits the lion then it eats the lion. If something likes the lion and it likes the squirrel then the lion eats the mouse. If the squirrel eats the lion then the lion is big. If something likes the mouse and the mouse visits the squirrel then the mouse is green. If something eats the mouse then it eats the lion. If something is green then it eats the mouse.
The lion is nice.
("lion" "is" "nice" "+")
The mouse is green.
("mouse" "is" "green" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
If the mouse is green then the mouse likes the lion.
((("mouse" "is" "green" "+")) -> ("mouse" "likes" "lion" "+"))
If something is red and it likes the mouse then it eats the mouse.
((("something" "is" "red" "+") ("something" "likes" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
If something visits the lion then it eats the lion.
((("something" "visits" "lion" "+")) -> ("something" "eats" "lion" "+"))
If something likes the lion and it likes the squirrel then the lion eats the mouse.
((("something" "likes" "lion" "+") ("something" "likes" "squirrel" "+")) -> ("lion" "eats" "mouse" "+"))
If the squirrel eats the lion then the lion is big.
((("squirrel" "eats" "lion" "+")) -> ("lion" "is" "big" "+"))
If something likes the mouse and the mouse visits the squirrel then the mouse is green.
((("something" "likes" "mouse" "+") ("mouse" "visits" "squirrel" "+")) -> ("mouse" "is" "green" "+"))
If something eats the mouse then it eats the lion.
((("something" "eats" "mouse" "+")) -> ("something" "eats" "lion" "+"))
If something is green then it eats the mouse.
((("something" "is" "green" "+")) -> ("something" "eats" "mouse" "+"))
The lion is nice.
True
1
proof
[(triple1)]
("lion" "is" "nice" "+")
triple1
The mouse is not green.
False
1
inv-proof
[(triple2)]
("mouse" "is" "green" "-")
triple2
The mouse likes the lion.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "likes" "lion" "+")
((triple2) -> (rule1 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The squirrel does not eat the mouse.
False
2
inv-proof
[(((triple3) -> rule8))]
("squirrel" "eats" "mouse" "-")
((triple3) -> (rule8 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel eats the lion.
True
3
proof
[(((((triple3) -> rule8)) -> rule7))]
("squirrel" "eats" "lion" "+")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The squirrel does not eat the lion.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule7))]
("squirrel" "eats" "lion" "-")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The lion is big.
True
4
proof
[(((((((triple3) -> rule8)) -> rule7)) -> rule5))]
("lion" "is" "big" "+")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3
The lion is not big.
False
4
inv-proof
[(((((((triple3) -> rule8)) -> rule7)) -> rule5))]
("lion" "is" "big" "-")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3
The lion does not eat the lion.
Unknown
inv-rconc
[@2: The lion eats the lion.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("lion" "eats" "lion" "-")
The lion eats the mouse.
Unknown
rconc
[@1: The lion eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "mouse" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The squirrel likes the lion.
Unknown
random
[@0: The squirrel likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "lion" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The mouse does not eat the squirrel.
Unknown
inv-random
[@0: The mouse eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "squirrel" "-")
The lion visits the mouse.
Unknown
random
[@0: The lion visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "mouse" "+")
@0: The lion is nice.[(triple1)] The mouse is green.[(triple2)] The squirrel is green.[(triple3)] @1: The mouse eats the mouse.[(((triple2) -> rule8))] The mouse likes the lion.[(((triple2) -> rule1))] The squirrel eats the mouse.[(((triple3) -> rule8))] @2: The mouse eats the lion.[(((((triple2) -> rule8)) -> rule7))] The squirrel eats the lion.[(((((triple3) -> rule8)) -> rule7))] @3: The lion is big.[(((((((triple3) -> rule8)) -> rule7)) -> rule5))]
The lion is nice.
("lion" "is" "nice" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The squirrel is green.
("squirrel" "is" "green" "+")
triple3
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple2) -> (rule8 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((triple2) -> (rule1 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
((triple3) -> (rule8 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The lion is big.
("lion" "is" "big" "+")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3