The cow eats the dog. The cow is rough. The cow needs the mouse. The cow does not see the dog. The dog is rough. The mouse is cold. The mouse is rough. The mouse is round. The mouse needs the dog. The mouse sees the dog. If someone needs the dog then the dog sees the cow. If someone sees the cow then they do not need the dog.
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow does not see the dog.
("cow" "sees" "dog" "-")
The dog is rough.
("dog" "is" "rough" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If someone needs the dog then the dog sees the cow.
((("someone" "needs" "dog" "+")) -> ("dog" "sees" "cow" "+"))
If someone sees the cow then they do not need the dog.
((("someone" "sees" "cow" "+")) -> ("someone" "needs" "dog" "-"))
The cow does not see the dog.
True
1
proof
[(triple4)]
("cow" "sees" "dog" "-")
triple4
The mouse is not cold.
False
1
inv-proof
[(triple6)]
("mouse" "is" "cold" "-")
triple6
The dog sees the cow.
True
2
proof
[(((triple9) -> rule1))]
("dog" "sees" "cow" "+")
((triple9) -> (rule1 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog does not see the cow.
False
2
inv-proof
[(((triple9) -> rule1))]
("dog" "sees" "cow" "-")
((triple9) -> (rule1 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog does not need the dog.
True
3
proof
[(((((triple9) -> rule1)) -> rule2))]
("dog" "needs" "dog" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The dog needs the dog.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule2))]
("dog" "needs" "dog" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The mouse does not see the cow.
Unknown
inv-random
[@0: The mouse sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cow" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow does not see the dog.[(triple4)] The cow eats the dog.[(triple1)] The cow is rough.[(triple2)] The cow needs the mouse.[(triple3)] The dog is rough.[(triple5)] The mouse is cold.[(triple6)] The mouse is rough.[(triple7)] The mouse is round.[(triple8)] The mouse needs the dog.[(triple9)] The mouse sees the dog.[(triple10)] @1: The dog sees the cow.[(((triple9) -> rule1))] @2: The dog does not need the dog.[(((((triple9) -> rule1)) -> rule2))]
The cow does not see the dog.
("cow" "sees" "dog" "-")
triple4
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple5
The mouse is cold.
("mouse" "is" "cold" "+")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
The mouse is round.
("mouse" "is" "round" "+")
triple8
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple9
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple10
The dog sees the cow.
("dog" "sees" "cow" "+")
((triple9) -> (rule1 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog does not need the dog.
("dog" "needs" "dog" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2