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