The bear likes the lion. The dog is kind. The lion is green. The lion is kind. The lion likes the rabbit. The lion needs the bear. The lion sees the rabbit. The rabbit is blue. The rabbit needs the lion. The rabbit sees the bear. The rabbit does not see the dog. If someone is blue and green then they see the bear. If the rabbit is red and the rabbit does not like the dog then the rabbit is green. If someone sees the rabbit then they do not need the dog. If someone sees the bear then they need the rabbit. If someone likes the lion then the lion sees the dog. If someone needs the rabbit then they see the lion. If someone sees the rabbit and the rabbit sees the lion then the lion sees the bear. If someone sees the rabbit then the rabbit needs the lion.
The bear likes the lion.
("bear" "likes" "lion" "+")
The dog is kind.
("dog" "is" "kind" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
If someone is blue and green then they see the bear.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "sees" "bear" "+"))
If the rabbit is red and the rabbit does not like the dog then the rabbit is green.
((("rabbit" "is" "red" "+") ("rabbit" "likes" "dog" "~")) -> ("rabbit" "is" "green" "+"))
If someone sees the rabbit then they do not need the dog.
((("someone" "sees" "rabbit" "+")) -> ("someone" "needs" "dog" "-"))
If someone sees the bear then they need the rabbit.
((("someone" "sees" "bear" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone likes the lion then the lion sees the dog.
((("someone" "likes" "lion" "+")) -> ("lion" "sees" "dog" "+"))
If someone needs the rabbit then they see the lion.
((("someone" "needs" "rabbit" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the rabbit and the rabbit sees the lion then the lion sees the bear.
((("someone" "sees" "rabbit" "+") ("rabbit" "sees" "lion" "+")) -> ("lion" "sees" "bear" "+"))
If someone sees the rabbit then the rabbit needs the lion.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "needs" "lion" "+"))
The lion needs the bear.
True
1
proof
[(triple6)]
("lion" "needs" "bear" "+")
triple6
The rabbit sees the dog.
False
1
inv-proof
[(triple11)]
("rabbit" "sees" "dog" "+")
triple11
The lion sees the dog.
True
2
proof
[(((triple1) -> rule5))]
("lion" "sees" "dog" "+")
((triple1) -> (rule5 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple10) -> rule4))]
("rabbit" "needs" "rabbit" "-")
((triple10) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the lion.
True
3
proof
[(((((triple10) -> rule4)) -> rule6))]
("rabbit" "sees" "lion" "+")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit does not see the lion.
False
3
inv-proof
[(((((triple10) -> rule4)) -> rule6))]
("rabbit" "sees" "lion" "-")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The lion sees the bear.
True
5
proof
[(((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule7))]
("lion" "sees" "bear" "+")
((triple7 ((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The lion does not see the bear.
False
5
inv-proof
[(((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule7))]
("lion" "sees" "bear" "-")
((triple7 ((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The lion needs the rabbit.
True
6
proof
[(((((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule4))]
("lion" "needs" "rabbit" "+")
((((triple7 ((((triple10) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int4
The lion does not need the rabbit.
False
6
inv-proof
[(((((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule4))]
("lion" "needs" "rabbit" "-")
((((triple7 ((((triple10) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int4
The lion sees the lion.
True
7
proof
[(((((((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule4)) -> rule6))]
("lion" "sees" "lion" "+")
((((((triple7 ((((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
int3
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int4
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int5
The lion does not see the lion.
False
7
inv-proof
[(((((((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule4)) -> rule6))]
("lion" "sees" "lion" "-")
((((((triple7 ((((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
int3
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int4
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int5
The dog does not see the bear.
Unknown
inv-rconc
[@1: The dog sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "bear" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "bear" "+")
The dog does not need the rabbit.
Unknown
inv-rconc
[@2: The dog needs the rabbit.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("dog" "needs" "rabbit" "-")
The bear sees the lion.
Unknown
rconc
[@3: The bear sees the lion.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule1 <- FAIL)]]
("bear" "sees" "lion" "+")
The bear does not need the rabbit.
Unknown
inv-rconc
[@2: The bear needs the rabbit.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("bear" "needs" "rabbit" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "green" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The rabbit needs the bear.
Unknown
random
[@0: The rabbit needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "bear" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The dog does not like the lion.
Unknown
inv-random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The bear likes the lion.[(triple1)] The dog is kind.[(triple2)] The lion is green.[(triple3)] The lion is kind.[(triple4)] The lion likes the rabbit.[(triple5)] The lion needs the bear.[(triple6)] The lion sees the rabbit.[(triple7)] The rabbit does not see the dog.[(triple11)] The rabbit is blue.[(triple8)] The rabbit needs the lion.[(triple9 OR ((triple7) -> rule8))] The rabbit sees the bear.[(triple10)] @1: The lion does not need the dog.[(((triple7) -> rule3))] The lion sees the dog.[(((triple1) -> rule5))] The rabbit needs the rabbit.[(((triple10) -> rule4))] @2: The rabbit sees the lion.[(((((triple10) -> rule4)) -> rule6))] @3: The lion sees the bear.[(((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule7))] @4: The lion needs the rabbit.[(((((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule4))] @5: The lion sees the lion.[(((((((triple7 ((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule4)) -> rule6))]
The bear likes the lion.
("bear" "likes" "lion" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
triple4
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple5
The lion needs the bear.
("lion" "needs" "bear" "+")
triple6
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple7
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
triple11
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple8
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple9
((triple7) -> (rule8 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple10
The lion does not need the dog.
("lion" "needs" "dog" "-")
((triple7) -> (rule3 % int1))
The lion does not need the dog.
("lion" "needs" "dog" "-")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
((triple1) -> (rule5 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple10) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
((triple7 ((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
((((triple7 ((((triple10) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int4
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((triple7 ((((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
int3
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int4
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int5