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