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