The cow does not need the squirrel. The dog is rough. The mouse does not need the cow. The squirrel is blue. If someone likes the dog then the dog likes the mouse. If someone needs the mouse then they need the dog. If the cow is big and the dog does not like the cow then the dog does not eat the mouse. If the cow is blue and the cow likes the squirrel then the squirrel likes the mouse. If someone likes the dog then they need the mouse. If someone is rough then they like the dog.
The cow does not need the squirrel.
("cow" "needs" "squirrel" "-")
The dog is rough.
("dog" "is" "rough" "+")
The mouse does not need the cow.
("mouse" "needs" "cow" "-")
The squirrel is blue.
("squirrel" "is" "blue" "+")
If someone likes the dog then the dog likes the mouse.
((("someone" "likes" "dog" "+")) -> ("dog" "likes" "mouse" "+"))
If someone needs the mouse then they need the dog.
((("someone" "needs" "mouse" "+")) -> ("someone" "needs" "dog" "+"))
If the cow is big and the dog does not like the cow then the dog does not eat the mouse.
((("cow" "is" "big" "+") ("dog" "likes" "cow" "~")) -> ("dog" "eats" "mouse" "-"))
If the cow is blue and the cow likes the squirrel then the squirrel likes the mouse.
((("cow" "is" "blue" "+") ("cow" "likes" "squirrel" "+")) -> ("squirrel" "likes" "mouse" "+"))
If someone likes the dog then they need the mouse.
((("someone" "likes" "dog" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is rough then they like the dog.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "dog" "+"))
The cow does not need the squirrel.
True
1
proof
[(triple1)]
("cow" "needs" "squirrel" "-")
triple1
The cow needs the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "needs" "squirrel" "+")
triple1
The dog likes the dog.
True
2
proof
[(((triple2) -> rule6))]
("dog" "likes" "dog" "+")
((triple2) -> (rule6 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog does not like the dog.
False
2
inv-proof
[(((triple2) -> rule6))]
("dog" "likes" "dog" "-")
((triple2) -> (rule6 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog needs the mouse.
True
3
proof
[(((((triple2) -> rule6)) -> rule5))]
("dog" "needs" "mouse" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog does not like the mouse.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule1))]
("dog" "likes" "mouse" "-")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog needs the dog.
True
4
proof
[(((((((triple2) -> rule6)) -> rule5)) -> rule2))]
("dog" "needs" "dog" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The dog does not need the dog.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule5)) -> rule2))]
("dog" "needs" "dog" "-")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The cow does not need the dog.
Unknown
inv-rconc
[@3: The cow needs the dog.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule6 <- FAIL)]]
("cow" "needs" "dog" "-")
The squirrel needs the dog.
Unknown
rconc
[@3: The squirrel needs the dog.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule6 <- FAIL)]]
("squirrel" "needs" "dog" "+")
The cow does not like the dog.
Unknown
inv-rconc
[@1: The cow likes the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "likes" "dog" "-")
The mouse needs the mouse.
Unknown
rconc
[@2: The mouse needs the mouse.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The squirrel does not need the cow.
Unknown
inv-random
[@0: The squirrel needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cow" "-")
The mouse eats the cow.
Unknown
random
[@0: The mouse eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cow" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The dog eats the cow.
Unknown
random
[@0: The dog eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cow" "+")
@0: The cow does not need the squirrel.[(triple1)] The dog is rough.[(triple2)] The mouse does not need the cow.[(triple3)] The squirrel is blue.[(triple4)] @1: The dog likes the dog.[(((triple2) -> rule6))] @2: The dog likes the mouse.[(((((triple2) -> rule6)) -> rule1))] The dog needs the mouse.[(((((triple2) -> rule6)) -> rule5))] @3: The dog needs the dog.[(((((((triple2) -> rule6)) -> rule5)) -> rule2))]
The cow does not need the squirrel.
("cow" "needs" "squirrel" "-")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The mouse does not need the cow.
("mouse" "needs" "cow" "-")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple4
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple2) -> (rule6 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3