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