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