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