The dog likes the mouse. The lion likes the dog. The mouse is young. The squirrel likes the dog. If someone is kind then they see the squirrel. If someone likes the dog then the dog needs the mouse. If someone needs the mouse then they like the squirrel.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The mouse is young.
("mouse" "is" "young" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
If someone is kind then they see the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone likes the dog then the dog needs the mouse.
((("someone" "likes" "dog" "+")) -> ("dog" "needs" "mouse" "+"))
If someone needs the mouse then they like the squirrel.
((("someone" "needs" "mouse" "+")) -> ("someone" "likes" "squirrel" "+"))
The lion likes the dog.
True
1
proof
[(triple2)]
("lion" "likes" "dog" "+")
triple2
The dog does not like the mouse.
False
1
inv-proof
[(triple1)]
("dog" "likes" "mouse" "-")
triple1
The dog needs the mouse.
True
2
proof
[(((triple2) -> rule2) OR ((triple4) -> rule2))]
("dog" "needs" "mouse" "+")
((triple2) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
((triple4) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog does not need the mouse.
False
2
inv-proof
[(((triple2) -> rule2) OR ((triple4) -> rule2))]
("dog" "needs" "mouse" "-")
((triple2) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
((triple4) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog likes the squirrel.
True
3
proof
[(((((triple2) -> rule2)) -> rule3) OR ((((triple4) -> rule2)) -> rule3))]
("dog" "likes" "squirrel" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog does not like the squirrel.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3) OR ((((triple4) -> rule2)) -> rule3))]
("dog" "likes" "squirrel" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The mouse likes the squirrel.
Unknown
rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "likes" "squirrel" "+")
The mouse does not see the squirrel.
Unknown
inv-rconc
[@1: The mouse sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "squirrel" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
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 squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
@0: The dog likes the mouse.[(triple1)] The lion likes the dog.[(triple2)] The mouse is young.[(triple3)] The squirrel likes the dog.[(triple4)] @1: The dog needs the mouse.[(((triple2) -> rule2) OR ((triple4) -> rule2))] @2: The dog likes the squirrel.[(((((triple2) -> rule2)) -> rule3) OR ((((triple4) -> rule2)) -> rule3))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The lion likes the dog.
("lion" "likes" "dog" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((triple2) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
((triple4) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2