The dog sees the rabbit. The mouse is red. The rabbit sees the mouse. If something eats the rabbit and it is not red then it sees the dog. If something sees the mouse then the mouse sees the rabbit. If something sees the rabbit then it does not eat the mouse. If something needs the rabbit then it is young. If something eats the dog and the dog needs the mouse then it eats the rabbit. If something sees the mouse then it is blue.
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The mouse is red.
("mouse" "is" "red" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something eats the rabbit and it is not red then it sees the dog.
((("something" "eats" "rabbit" "+") ("something" "is" "red" "~")) -> ("something" "sees" "dog" "+"))
If something sees the mouse then the mouse sees the rabbit.
((("something" "sees" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
If something sees the rabbit then it does not eat the mouse.
((("something" "sees" "rabbit" "+")) -> ("something" "eats" "mouse" "-"))
If something needs the rabbit then it is young.
((("something" "needs" "rabbit" "+")) -> ("something" "is" "young" "+"))
If something eats the dog and the dog needs the mouse then it eats the rabbit.
((("something" "eats" "dog" "+") ("dog" "needs" "mouse" "+")) -> ("something" "eats" "rabbit" "+"))
If something sees the mouse then it is blue.
((("something" "sees" "mouse" "+")) -> ("something" "is" "blue" "+"))
The dog sees the rabbit.
True
1
proof
[(triple1)]
("dog" "sees" "rabbit" "+")
triple1
The mouse is not red.
False
1
inv-proof
[(triple2)]
("mouse" "is" "red" "-")
triple2
The dog does not eat the mouse.
True
2
proof
[(((triple1) -> rule3))]
("dog" "eats" "mouse" "-")
((triple1) -> (rule3 % int1))
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple3) -> rule6))]
("rabbit" "is" "blue" "-")
((triple3) -> (rule6 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The mouse does not eat the mouse.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "eats" "mouse" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The mouse eats the mouse.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "eats" "mouse" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The mouse does not see the dog.
Unknown
inv-rconc
[@1: The mouse sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "dog" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "blue" "+")
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "young" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The mouse needs the rabbit.
Unknown
random
[@0: The mouse needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "rabbit" "+")
@0: The dog sees the rabbit.[(triple1)] The mouse is red.[(triple2)] The rabbit sees the mouse.[(triple3)] @1: The dog does not eat the mouse.[(((triple1) -> rule3))] The mouse sees the rabbit.[(((triple3) -> rule2))] The rabbit is blue.[(((triple3) -> rule6))] @2: The mouse does not eat the mouse.[(((((triple3) -> rule2)) -> rule3))]
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple3
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
((triple1) -> (rule3 % int1))
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
((triple3) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple3) -> (rule6 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2