The lion needs the squirrel. The squirrel eats the lion. The squirrel is big. If someone eats the lion then the lion eats the squirrel. If someone eats the lion then the lion eats the squirrel. If someone eats the squirrel then the squirrel likes the lion. If the lion is green then the lion is big. If the squirrel needs the lion then the squirrel eats the lion. If someone likes the lion and they are green then the lion eats the squirrel. If the lion eats the squirrel then the squirrel is blue. If someone eats the lion and they eat the squirrel then the squirrel eats the lion.
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
If someone eats the lion then the lion eats the squirrel.
((("someone" "eats" "lion" "+")) -> ("lion" "eats" "squirrel" "+"))
If someone eats the lion then the lion eats the squirrel.
((("someone" "eats" "lion" "+")) -> ("lion" "eats" "squirrel" "+"))
If someone eats the squirrel then the squirrel likes the lion.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "likes" "lion" "+"))
If the lion is green then the lion is big.
((("lion" "is" "green" "+")) -> ("lion" "is" "big" "+"))
If the squirrel needs the lion then the squirrel eats the lion.
((("squirrel" "needs" "lion" "+")) -> ("squirrel" "eats" "lion" "+"))
If someone likes the lion and they are green then the lion eats the squirrel.
((("someone" "likes" "lion" "+") ("someone" "is" "green" "+")) -> ("lion" "eats" "squirrel" "+"))
If the lion eats the squirrel then the squirrel is blue.
((("lion" "eats" "squirrel" "+")) -> ("squirrel" "is" "blue" "+"))
If someone eats the lion and they eat the squirrel then the squirrel eats the lion.
((("someone" "eats" "lion" "+") ("someone" "eats" "squirrel" "+")) -> ("squirrel" "eats" "lion" "+"))
The lion needs the squirrel.
True
1
proof
[(triple1)]
("lion" "needs" "squirrel" "+")
triple1
The squirrel does not eat the lion.
False
1
inv-proof
[(triple2)]
("squirrel" "eats" "lion" "-")
triple2
The lion eats the squirrel.
True
2
proof
[(((triple2) -> rule1) OR ((triple2) -> rule2))]
("lion" "eats" "squirrel" "+")
((triple2) -> (rule1 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
((triple2) -> (rule2 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion does not eat the squirrel.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple2) -> rule2))]
("lion" "eats" "squirrel" "-")
((triple2) -> (rule1 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
((triple2) -> (rule2 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The squirrel likes the lion.
True
3
proof
[(((((triple2) -> rule1)) -> rule3) OR ((((triple2) -> rule2)) -> rule3))]
("squirrel" "likes" "lion" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The squirrel does not like the lion.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3) OR ((((triple2) -> rule2)) -> rule3))]
("squirrel" "likes" "lion" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "big" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion needs the squirrel.[(triple1)] The squirrel eats the lion.[(triple2)] The squirrel is big.[(triple3)] @1: The lion eats the squirrel.[(((triple2) -> rule1) OR ((triple2) -> rule2))] @2: The squirrel is blue.[(((((triple2) -> rule1)) -> rule7) OR ((((triple2) -> rule2)) -> rule7))] The squirrel likes the lion.[(((((triple2) -> rule1)) -> rule3) OR ((((triple2) -> rule2)) -> rule3))]
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple2
The squirrel is big.
("squirrel" "is" "big" "+")
triple3
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
((triple2) -> (rule1 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
((triple2) -> (rule2 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2