The lion eats the squirrel. The lion is young. The lion needs the rabbit. The lion needs the squirrel. The lion visits the squirrel. The rabbit is green. The rabbit is red. The rabbit is young. The rabbit visits the lion. The squirrel is big. The squirrel is green. The squirrel needs the rabbit. If someone visits the rabbit then they eat the lion. If someone needs the lion then they visit the squirrel. If someone visits the rabbit then they eat the squirrel. If someone eats the squirrel then the squirrel needs the lion. If someone is big and they eat the lion then the lion is green. If the lion needs the rabbit then the rabbit is big.
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If someone visits the rabbit then they eat the lion.
((("someone" "visits" "rabbit" "+")) -> ("someone" "eats" "lion" "+"))
If someone needs the lion then they visit the squirrel.
((("someone" "needs" "lion" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the rabbit then they eat the squirrel.
((("someone" "visits" "rabbit" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone eats the squirrel then the squirrel needs the lion.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "needs" "lion" "+"))
If someone is big and they eat the lion then the lion is green.
((("someone" "is" "big" "+") ("someone" "eats" "lion" "+")) -> ("lion" "is" "green" "+"))
If the lion needs the rabbit then the rabbit is big.
((("lion" "needs" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
The lion eats the squirrel.
True
1
proof
[(triple1)]
("lion" "eats" "squirrel" "+")
triple1
The rabbit is not young.
False
1
inv-proof
[(triple8)]
("rabbit" "is" "young" "-")
triple8
The squirrel needs the lion.
True
2
proof
[(((triple1) -> rule4))]
("squirrel" "needs" "lion" "+")
((triple1) -> (rule4 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel does not need the lion.
False
2
inv-proof
[(((triple1) -> rule4))]
("squirrel" "needs" "lion" "-")
((triple1) -> (rule4 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel visits the squirrel.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("squirrel" "visits" "squirrel" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel does not visit the squirrel.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("squirrel" "visits" "squirrel" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The rabbit does not eat the lion.
Unknown
inv-rconc
[@1: The rabbit eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "lion" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "lion" "+")
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The squirrel eats the rabbit.
Unknown
random
[@0: The squirrel eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "rabbit" "+")
@0: The lion eats the squirrel.[(triple1)] The lion is young.[(triple2)] The lion needs the rabbit.[(triple3)] The lion needs the squirrel.[(triple4)] The lion visits the squirrel.[(triple5)] The rabbit is green.[(triple6)] The rabbit is red.[(triple7)] The rabbit is young.[(triple8)] The rabbit visits the lion.[(triple9)] The squirrel is big.[(triple10)] The squirrel is green.[(triple11)] The squirrel needs the rabbit.[(triple12)] @1: The rabbit is big.[(((triple3) -> rule6))] The squirrel needs the lion.[(((triple1) -> rule4))] @2: The squirrel visits the squirrel.[(((((triple1) -> rule4)) -> rule2))]
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple3
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple4
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple5
The rabbit is green.
("rabbit" "is" "green" "+")
triple6
The rabbit is red.
("rabbit" "is" "red" "+")
triple7
The rabbit is young.
("rabbit" "is" "young" "+")
triple8
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple9
The squirrel is big.
("squirrel" "is" "big" "+")
triple10
The squirrel is green.
("squirrel" "is" "green" "+")
triple11
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple12
The rabbit is big.
("rabbit" "is" "big" "+")
((triple3) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
((triple1) -> (rule4 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2