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