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