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