The bear is red. The bear does not like the lion. The dog does not need the lion. The dog does not see the lion. The dog sees the mouse. The lion is kind. The lion likes the bear. The lion needs the dog. The mouse is rough. The mouse likes the bear. If the lion is blue and the lion needs the mouse then the mouse is rough. If something sees the bear then it likes the mouse. If something is red then it sees the bear.
The bear is red.
("bear" "is" "red" "+")
The bear does not like the lion.
("bear" "likes" "lion" "-")
The dog does not need the lion.
("dog" "needs" "lion" "-")
The dog does not see the lion.
("dog" "sees" "lion" "-")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
If the lion is blue and the lion needs the mouse then the mouse is rough.
((("lion" "is" "blue" "+") ("lion" "needs" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If something sees the bear then it likes the mouse.
((("something" "sees" "bear" "+")) -> ("something" "likes" "mouse" "+"))
If something is red then it sees the bear.
((("something" "is" "red" "+")) -> ("something" "sees" "bear" "+"))
The bear is red.
True
1
proof
[(triple1)]
("bear" "is" "red" "+")
triple1
The bear is not red.
False
1
inv-proof
[(triple1)]
("bear" "is" "red" "-")
triple1
The bear sees the bear.
True
2
proof
[(((triple1) -> rule3))]
("bear" "sees" "bear" "+")
((triple1) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear does not see the bear.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "sees" "bear" "-")
((triple1) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear likes the mouse.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("bear" "likes" "mouse" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear does not like the mouse.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("bear" "likes" "mouse" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The mouse does not see the bear.
Unknown
inv-rconc
[@1: The mouse sees the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "bear" "-")
The lion likes the mouse.
Unknown
rconc
[@2: The lion likes the mouse.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("lion" "likes" "mouse" "+")
The lion does not see the bear.
Unknown
inv-rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "bear" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The bear needs the mouse.
Unknown
random
[@0: The bear needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "mouse" "+")
@0: The bear does not like the lion.[(triple2)] The bear is red.[(triple1)] The dog does not need the lion.[(triple3)] The dog does not see the lion.[(triple4)] The dog sees the mouse.[(triple5)] The lion is kind.[(triple6)] The lion likes the bear.[(triple7)] The lion needs the dog.[(triple8)] The mouse is rough.[(triple9)] The mouse likes the bear.[(triple10)] @1: The bear sees the bear.[(((triple1) -> rule3))] @2: The bear likes the mouse.[(((((triple1) -> rule3)) -> rule2))]
The bear does not like the lion.
("bear" "likes" "lion" "-")
triple2
The bear is red.
("bear" "is" "red" "+")
triple1
The dog does not need the lion.
("dog" "needs" "lion" "-")
triple3
The dog does not see the lion.
("dog" "sees" "lion" "-")
triple4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple5
The lion is kind.
("lion" "is" "kind" "+")
triple6
The lion likes the bear.
("lion" "likes" "bear" "+")
triple7
The lion needs the dog.
("lion" "needs" "dog" "+")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple10
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple1) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2