The bear likes the mouse. The dog is red. The lion visits the mouse. The mouse needs the bear. If someone likes the lion then the lion is kind. If someone needs the dog then the dog visits the bear. If someone is kind and they like the dog then the dog likes the bear. If someone is round then they like the bear. If someone needs the lion and they like the dog then the lion needs the dog. If someone likes the mouse then the mouse is kind. If someone is cold and they like the mouse then the mouse likes the lion. Kind people are round.
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The dog is red.
("dog" "is" "red" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
If someone likes the lion then the lion is kind.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "kind" "+"))
If someone needs the dog then the dog visits the bear.
((("someone" "needs" "dog" "+")) -> ("dog" "visits" "bear" "+"))
If someone is kind and they like the dog then the dog likes the bear.
((("someone" "is" "kind" "+") ("someone" "likes" "dog" "+")) -> ("dog" "likes" "bear" "+"))
If someone is round then they like the bear.
((("someone" "is" "round" "+")) -> ("someone" "likes" "bear" "+"))
If someone needs the lion and they like the dog then the lion needs the dog.
((("someone" "needs" "lion" "+") ("someone" "likes" "dog" "+")) -> ("lion" "needs" "dog" "+"))
If someone likes the mouse then the mouse is kind.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If someone is cold and they like the mouse then the mouse likes the lion.
((("someone" "is" "cold" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
Kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
The bear likes the mouse.
True
1
proof
[(triple1)]
("bear" "likes" "mouse" "+")
triple1
The bear does not like the mouse.
False
1
inv-proof
[(triple1)]
("bear" "likes" "mouse" "-")
triple1
The mouse is kind.
True
2
proof
[(((triple1) -> rule6))]
("mouse" "is" "kind" "+")
((triple1) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple1) -> rule6))]
("mouse" "is" "kind" "-")
((triple1) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is round.
True
3
proof
[(((((triple1) -> rule6)) -> rule8))]
("mouse" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is not round.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule8))]
("mouse" "is" "round" "-")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the bear.
True
4
proof
[(((((((triple1) -> rule6)) -> rule8)) -> rule4))]
("mouse" "likes" "bear" "+")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse does not like the bear.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule8)) -> rule4))]
("mouse" "likes" "bear" "-")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The dog does not like the bear.
Unknown
inv-rconc
[@2: The dog likes the bear.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("dog" "likes" "bear" "-")
The lion is round.
Unknown
rconc
[@3: The lion is round.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule7 <- FAIL)]]
("lion" "is" "round" "+")
The mouse does not like the lion.
Unknown
inv-rconc
[@1: The mouse likes the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "likes" "lion" "-")
The dog visits the bear.
Unknown
rconc
[@2: The dog visits the bear.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("dog" "visits" "bear" "+")
The dog does not visit the lion.
Unknown
inv-random
[@0: The dog visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "lion" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The bear likes the mouse.[(triple1)] The dog is red.[(triple2)] The lion visits the mouse.[(triple3)] The mouse needs the bear.[(triple4)] @1: The mouse is kind.[(((triple1) -> rule6))] @2: The mouse is round.[(((((triple1) -> rule6)) -> rule8))] @3: The mouse likes the bear.[(((((((triple1) -> rule6)) -> rule8)) -> rule4))]
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple3
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
((triple1) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3