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