The lion is green. The lion is nice. The lion is red. The lion is young. The lion needs the rabbit. The lion sees the rabbit. The lion visits the rabbit. The rabbit is nice. The rabbit is young. The rabbit needs the lion. The rabbit sees the lion. The rabbit visits the lion. If something needs the lion and the lion visits the rabbit then it is blue. If the rabbit visits the lion and the rabbit sees the lion then the rabbit is blue. If something visits the lion and it is blue then it needs the rabbit. If something sees the rabbit and the rabbit visits the lion then the rabbit sees the lion. If something sees the rabbit then the rabbit sees the lion. If something sees the rabbit then the rabbit is blue. If something visits the lion and it is green then it visits the rabbit. If something needs the lion and it is young then the lion sees the rabbit.
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something needs the lion and the lion visits the rabbit then it is blue.
((("something" "needs" "lion" "+") ("lion" "visits" "rabbit" "+")) -> ("something" "is" "blue" "+"))
If the rabbit visits the lion and the rabbit sees the lion then the rabbit is blue.
((("rabbit" "visits" "lion" "+") ("rabbit" "sees" "lion" "+")) -> ("rabbit" "is" "blue" "+"))
If something visits the lion and it is blue then it needs the rabbit.
((("something" "visits" "lion" "+") ("something" "is" "blue" "+")) -> ("something" "needs" "rabbit" "+"))
If something sees the rabbit and the rabbit visits the lion then the rabbit sees the lion.
((("something" "sees" "rabbit" "+") ("rabbit" "visits" "lion" "+")) -> ("rabbit" "sees" "lion" "+"))
If something sees the rabbit then the rabbit sees the lion.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
If something sees the rabbit then the rabbit is blue.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
If something visits the lion and it is green then it visits the rabbit.
((("something" "visits" "lion" "+") ("something" "is" "green" "+")) -> ("something" "visits" "rabbit" "+"))
If something needs the lion and it is young then the lion sees the rabbit.
((("something" "needs" "lion" "+") ("something" "is" "young" "+")) -> ("lion" "sees" "rabbit" "+"))
The lion needs the rabbit.
True
1
proof
[(triple5)]
("lion" "needs" "rabbit" "+")
triple5
The lion does not need the rabbit.
False
1
inv-proof
[(triple5)]
("lion" "needs" "rabbit" "-")
triple5
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The lion is green.[(triple1)] The lion is nice.[(triple2)] The lion is red.[(triple3)] The lion is young.[(triple4)] The lion needs the rabbit.[(triple5)] The lion sees the rabbit.[(triple6 OR ((triple10 triple9) -> rule8))] The lion visits the rabbit.[(triple7)] The rabbit is nice.[(triple8)] The rabbit is young.[(triple9)] The rabbit needs the lion.[(triple10)] The rabbit sees the lion.[(triple11 OR ((triple6) -> rule5) OR ((triple6 triple12) -> rule4) OR ((((triple10 triple9) -> rule8)) -> rule5) OR ((((triple10 triple9) -> rule8) triple12) -> rule4))] The rabbit visits the lion.[(triple12)] @1: The rabbit is blue.[(((triple6) -> rule6) OR ((triple10 triple7) -> rule1) OR ((triple12 triple11) -> rule2) OR ((((triple10 triple9) -> rule8)) -> rule6) OR ((triple12 ((triple6) -> rule5)) -> rule2) OR ((triple12 ((triple6 triple12) -> rule4)) -> rule2) OR ((triple12 ((((triple10 triple9) -> rule8)) -> rule5)) -> rule2) OR ((triple12 ((((triple10 triple9) -> rule8) triple12) -> rule4)) -> rule2))] @2: The rabbit needs the rabbit.[(((triple12 ((triple6) -> rule6)) -> rule3) OR ((triple12 ((triple10 triple7) -> rule1)) -> rule3) OR ((triple12 ((triple12 triple11) -> rule2)) -> rule3) OR ((triple12 ((((triple10 triple9) -> rule8)) -> rule6)) -> rule3) OR ((triple12 ((triple12 ((triple6) -> rule5)) -> rule2)) -> rule3) OR ((triple12 ((triple12 ((triple6 triple12) -> rule4)) -> rule2)) -> rule3) OR ((triple12 ((triple12 ((((triple10 triple9) -> rule8)) -> rule5)) -> rule2)) -> rule3) OR ((triple12 ((triple12 ((((triple10 triple9) -> rule8) triple12) -> rule4)) -> rule2)) -> rule3))]
The lion is green.
("lion" "is" "green" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
triple4
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple5
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple6
((triple10 triple9) -> (rule8 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The rabbit is young.
("rabbit" "is" "young" "+")
triple9
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple10
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple11
((triple6) -> (rule5 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
((triple6 triple12) -> (rule4 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
((((triple10 triple9) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int2
((((triple10 triple9) -> (rule8 % int2)) triple12) -> (rule4 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int2
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple12
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple6) -> (rule6 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((triple10 triple7) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((triple12 triple11) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((((triple10 triple9) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int2
((triple12 ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
((triple12 ((triple6 triple12) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
((triple12 ((((triple10 triple9) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int3
((triple12 ((((triple10 triple9) -> (rule8 % int3)) triple12) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple12 ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((triple12 ((triple10 triple7) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((triple12 ((triple12 triple11) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((triple12 ((((triple10 triple9) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int3
((triple12 ((triple12 ((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
((triple12 ((triple12 ((triple6 triple12) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
((triple12 ((triple12 ((((triple10 triple9) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int4
((triple12 ((triple12 ((((triple10 triple9) -> (rule8 % int4)) triple12) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int4