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