The cow is kind. The cow is nice. The cow needs the mouse. The cow sees the mouse. The dog eats the cow. The dog eats the mouse. The dog is cold. The dog is kind. The dog is nice. The dog sees the mouse. The mouse eats the cow. The mouse eats the dog. The mouse is nice. The mouse needs the dog. The mouse sees the cow. The mouse sees the dog. If the cow eats the dog then the dog needs the cow. If someone is big and they need the dog then they eat the dog. If someone sees the dog and the dog eats the cow then they eat the cow. If someone eats the dog and the dog is nice then they need the mouse. If someone eats the dog and the dog needs the cow then the dog eats the mouse. If someone needs the cow and the cow needs the mouse then they are nice.
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is nice.
("dog" "is" "nice" "+")
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 nice.
("mouse" "is" "nice" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If the cow eats the dog then the dog needs the cow.
((("cow" "eats" "dog" "+")) -> ("dog" "needs" "cow" "+"))
If someone is big and they need the dog then they eat the dog.
((("someone" "is" "big" "+") ("someone" "needs" "dog" "+")) -> ("someone" "eats" "dog" "+"))
If someone sees the dog and the dog eats the cow then they eat the cow.
((("someone" "sees" "dog" "+") ("dog" "eats" "cow" "+")) -> ("someone" "eats" "cow" "+"))
If someone eats the dog and the dog is nice then they need the mouse.
((("someone" "eats" "dog" "+") ("dog" "is" "nice" "+")) -> ("someone" "needs" "mouse" "+"))
If someone eats the dog and the dog needs the cow then the dog eats the mouse.
((("someone" "eats" "dog" "+") ("dog" "needs" "cow" "+")) -> ("dog" "eats" "mouse" "+"))
If someone needs the cow and the cow needs the mouse then they are nice.
((("someone" "needs" "cow" "+") ("cow" "needs" "mouse" "+")) -> ("someone" "is" "nice" "+"))
The cow sees the mouse.
True
1
proof
[(triple4)]
("cow" "sees" "mouse" "+")
triple4
The mouse does not see the dog.
False
1
inv-proof
[(triple16)]
("mouse" "sees" "dog" "-")
triple16
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "cow" "-")
The cow sees the dog.
Unknown
random
[@0: The cow sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "dog" "+")
@0: The cow is kind.[(triple1)] The cow is nice.[(triple2)] The cow needs the mouse.[(triple3)] The cow sees the mouse.[(triple4)] The dog eats the cow.[(triple5)] The dog eats the mouse.[(triple6)] The dog is cold.[(triple7)] The dog is kind.[(triple8)] The dog is nice.[(triple9)] The dog sees the mouse.[(triple10)] The mouse eats the cow.[(triple11 OR ((triple16 triple5) -> rule3))] The mouse eats the dog.[(triple12)] The mouse is nice.[(triple13)] The mouse needs the dog.[(triple14)] The mouse sees the cow.[(triple15)] The mouse sees the dog.[(triple16)] @1: The mouse needs the mouse.[(((triple12 triple9) -> rule4))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple4
The dog eats the cow.
("dog" "eats" "cow" "+")
triple5
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple6
The dog is cold.
("dog" "is" "cold" "+")
triple7
The dog is kind.
("dog" "is" "kind" "+")
triple8
The dog is nice.
("dog" "is" "nice" "+")
triple9
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple10
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple11
((triple16 triple5) -> (rule3 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple12
The mouse is nice.
("mouse" "is" "nice" "+")
triple13
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple14
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple15
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple16
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple12 triple9) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1