The lion chases the squirrel. The rabbit eats the lion. The squirrel is rough. If someone needs the rabbit then the rabbit needs the squirrel. If someone eats the squirrel and they need the lion then the lion is cold. If someone eats the lion and they are green then they eat the rabbit. If someone is kind and they eat the lion then they need the rabbit. If someone chases the rabbit and the rabbit needs the lion then they eat the rabbit. If someone chases the rabbit then they chase the lion. If someone needs the squirrel then the squirrel chases the rabbit. If someone eats the lion then the lion needs the rabbit.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If someone needs the rabbit then the rabbit needs the squirrel.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "needs" "squirrel" "+"))
If someone eats the squirrel and they need the lion then the lion is cold.
((("someone" "eats" "squirrel" "+") ("someone" "needs" "lion" "+")) -> ("lion" "is" "cold" "+"))
If someone eats the lion and they are green then they eat the rabbit.
((("someone" "eats" "lion" "+") ("someone" "is" "green" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is kind and they eat the lion then they need the rabbit.
((("someone" "is" "kind" "+") ("someone" "eats" "lion" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone chases the rabbit and the rabbit needs the lion then they eat the rabbit.
((("someone" "chases" "rabbit" "+") ("rabbit" "needs" "lion" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone chases the rabbit then they chase the lion.
((("someone" "chases" "rabbit" "+")) -> ("someone" "chases" "lion" "+"))
If someone needs the squirrel then the squirrel chases the rabbit.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "chases" "rabbit" "+"))
If someone eats the lion then the lion needs the rabbit.
((("someone" "eats" "lion" "+")) -> ("lion" "needs" "rabbit" "+"))
The squirrel is rough.
True
1
proof
[(triple3)]
("squirrel" "is" "rough" "+")
triple3
The lion does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("lion" "chases" "squirrel" "-")
triple1
The lion needs the rabbit.
True
2
proof
[(((triple2) -> rule8))]
("lion" "needs" "rabbit" "+")
((triple2) -> (rule8 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion does not need the rabbit.
False
2
inv-proof
[(((triple2) -> rule8))]
("lion" "needs" "rabbit" "-")
((triple2) -> (rule8 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The rabbit needs the squirrel.
True
3
proof
[(((((triple2) -> rule8)) -> rule1))]
("rabbit" "needs" "squirrel" "+")
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The rabbit does not need the squirrel.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule1))]
("rabbit" "needs" "squirrel" "-")
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The squirrel chases the rabbit.
True
4
proof
[(((((((triple2) -> rule8)) -> rule1)) -> rule7))]
("squirrel" "chases" "rabbit" "+")
((((((triple2) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int3
The squirrel does not chase the rabbit.
False
4
inv-proof
[(((((((triple2) -> rule8)) -> rule1)) -> rule7))]
("squirrel" "chases" "rabbit" "-")
((((((triple2) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int3
The squirrel does not eat the rabbit.
Unknown
inv-rconc
[@1: The squirrel eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "eats" "rabbit" "-")
The lion eats the rabbit.
Unknown
rconc
[@1: The lion eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "eats" "rabbit" "+")
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The lion chases the lion.
Unknown
rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "chases" "lion" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The lion eats the squirrel.
Unknown
random
[@0: The lion eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "squirrel" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The lion chases the squirrel.[(triple1)] The rabbit eats the lion.[(triple2)] The squirrel is rough.[(triple3)] @1: The lion needs the rabbit.[(((triple2) -> rule8))] @2: The rabbit needs the squirrel.[(((((triple2) -> rule8)) -> rule1))] @3: The squirrel chases the rabbit.[(((((((triple2) -> rule8)) -> rule1)) -> rule7))] @4: The squirrel chases the lion.[(((((((((triple2) -> rule8)) -> rule1)) -> rule7)) -> rule6))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple3
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
((triple2) -> (rule8 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
((((((triple2) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int3
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
((((((((triple2) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int2
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int3
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int4