The dog needs the mouse. The mouse chases the dog. If something is red and it needs the mouse then it chases the dog. If something chases the dog then it needs the mouse. If something needs the mouse then it chases the mouse. If the dog needs the mouse then the mouse chases the dog. If something eats the dog and the dog is kind then the dog eats the mouse. If something is round and it needs the dog then the dog eats the mouse. If something eats the dog and it needs the dog then the dog is big. If something needs the mouse then the mouse is blue.
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
If something is red and it needs the mouse then it chases the dog.
((("something" "is" "red" "+") ("something" "needs" "mouse" "+")) -> ("something" "chases" "dog" "+"))
If something chases the dog then it needs the mouse.
((("something" "chases" "dog" "+")) -> ("something" "needs" "mouse" "+"))
If something needs the mouse then it chases the mouse.
((("something" "needs" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If the dog needs the mouse then the mouse chases the dog.
((("dog" "needs" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If something eats the dog and the dog is kind then the dog eats the mouse.
((("something" "eats" "dog" "+") ("dog" "is" "kind" "+")) -> ("dog" "eats" "mouse" "+"))
If something is round and it needs the dog then the dog eats the mouse.
((("something" "is" "round" "+") ("something" "needs" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
If something eats the dog and it needs the dog then the dog is big.
((("something" "eats" "dog" "+") ("something" "needs" "dog" "+")) -> ("dog" "is" "big" "+"))
If something needs the mouse then the mouse is blue.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
The mouse chases the dog.
True
1
proof
[(triple2 OR ((triple1) -> rule4))]
("mouse" "chases" "dog" "+")
triple2
((triple1) -> (rule4 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse does not chase the dog.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule4))]
("mouse" "chases" "dog" "-")
triple2
((triple1) -> (rule4 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse needs the mouse.
True
2
proof
[(((triple2) -> rule2) OR ((((triple1) -> rule4)) -> rule2))]
("mouse" "needs" "mouse" "+")
((triple2) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The mouse is not blue.
False
2
inv-proof
[(((triple1) -> rule8) OR ((((triple2) -> rule2)) -> rule8) OR ((((((triple1) -> rule4)) -> rule2)) -> rule8))]
("mouse" "is" "blue" "-")
((triple1) -> (rule8 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The mouse chases the mouse.
True
3
proof
[(((((triple2) -> rule2)) -> rule3) OR ((((((triple1) -> rule4)) -> rule2)) -> rule3))]
("mouse" "chases" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The mouse does not chase the mouse.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3) OR ((((((triple1) -> rule4)) -> rule2)) -> rule3))]
("mouse" "chases" "mouse" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The dog does not eat the mouse.
Unknown
inv-rconc
[@1: The dog eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "mouse" "-")
The dog is big.
Unknown
rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "big" "+")
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "dog" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The dog needs the mouse.[(triple1)] The mouse chases the dog.[(triple2 OR ((triple1) -> rule4))] @1: The dog chases the mouse.[(((triple1) -> rule3))] The mouse is blue.[(((triple1) -> rule8) OR ((((triple2) -> rule2)) -> rule8) OR ((((((triple1) -> rule4)) -> rule2)) -> rule8))] The mouse needs the mouse.[(((triple2) -> rule2) OR ((((triple1) -> rule4)) -> rule2))] @2: The mouse chases the mouse.[(((((triple2) -> rule2)) -> rule3) OR ((((((triple1) -> rule4)) -> rule2)) -> rule3))]
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple2
((triple1) -> (rule4 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((triple1) -> (rule3 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((triple1) -> (rule8 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple2) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3