The cow chases the dog. The cow is kind. The cow sees the mouse. The dog eats the cow. The dog is blue. The dog is green. The dog sees the mouse. The mouse eats the cow. The mouse eats the dog. The mouse is blue. The mouse sees the cow. The mouse sees the dog. If someone sees the cow then they chase the cow. If someone is rough then they chase the mouse.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If someone sees the cow then they chase the cow.
((("someone" "sees" "cow" "+")) -> ("someone" "chases" "cow" "+"))
If someone is rough then they chase the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "mouse" "+"))
The mouse is blue.
True
1
proof
[(triple10)]
("mouse" "is" "blue" "+")
triple10
The dog is not blue.
False
1
inv-proof
[(triple5)]
("dog" "is" "blue" "-")
triple5
The mouse chases the cow.
True
2
proof
[(((triple11) -> rule1))]
("mouse" "chases" "cow" "+")
((triple11) -> (rule1 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The mouse does not chase the cow.
False
2
inv-proof
[(((triple11) -> rule1))]
("mouse" "chases" "cow" "-")
((triple11) -> (rule1 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "cow" "-")
The dog chases the mouse.
Unknown
rconc
[@1: The dog chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "mouse" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The cow chases the dog.[(triple1)] The cow is kind.[(triple2)] The cow sees the mouse.[(triple3)] The dog eats the cow.[(triple4)] The dog is blue.[(triple5)] The dog is green.[(triple6)] The dog sees the mouse.[(triple7)] The mouse eats the cow.[(triple8)] The mouse eats the dog.[(triple9)] The mouse is blue.[(triple10)] The mouse sees the cow.[(triple11)] The mouse sees the dog.[(triple12)] @1: The mouse chases the cow.[(((triple11) -> rule1))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple3
The dog eats the cow.
("dog" "eats" "cow" "+")
triple4
The dog is blue.
("dog" "is" "blue" "+")
triple5
The dog is green.
("dog" "is" "green" "+")
triple6
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple7
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple8
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple11
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple12
The mouse chases the cow.
("mouse" "chases" "cow" "+")
((triple11) -> (rule1 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1