The bear visits the dog. The cow is big. The cow sees the bear. The cow does not see the dog. The dog sees the bear. The mouse is big. The mouse sees the cow. If something sees the cow then the cow visits the bear. If something visits the bear then it does not see the mouse. If something sees the mouse then the mouse visits the bear. If something visits the mouse then it does not like the cow. If something visits the dog then the dog sees the mouse. If the mouse likes the cow then the cow does not like the mouse.
The bear visits the dog.
("bear" "visits" "dog" "+")
The cow is big.
("cow" "is" "big" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow does not see the dog.
("cow" "sees" "dog" "-")
The dog sees the bear.
("dog" "sees" "bear" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something sees the cow then the cow visits the bear.
((("something" "sees" "cow" "+")) -> ("cow" "visits" "bear" "+"))
If something visits the bear then it does not see the mouse.
((("something" "visits" "bear" "+")) -> ("something" "sees" "mouse" "-"))
If something sees the mouse then the mouse visits the bear.
((("something" "sees" "mouse" "+")) -> ("mouse" "visits" "bear" "+"))
If something visits the mouse then it does not like the cow.
((("something" "visits" "mouse" "+")) -> ("something" "likes" "cow" "-"))
If something visits the dog then the dog sees the mouse.
((("something" "visits" "dog" "+")) -> ("dog" "sees" "mouse" "+"))
If the mouse likes the cow then the cow does not like the mouse.
((("mouse" "likes" "cow" "+")) -> ("cow" "likes" "mouse" "-"))
The cow does not see the dog.
True
1
proof
[(triple4)]
("cow" "sees" "dog" "-")
triple4
The cow sees the dog.
False
1
inv-proof
[(triple4)]
("cow" "sees" "dog" "+")
triple4
The cow visits the bear.
True
2
proof
[(((triple7) -> rule1))]
("cow" "visits" "bear" "+")
((triple7) -> (rule1 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The dog does not see the mouse.
False
2
inv-proof
[(((triple1) -> rule5))]
("dog" "sees" "mouse" "-")
((triple1) -> (rule5 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The mouse visits the bear.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("mouse" "visits" "bear" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The mouse does not visit the bear.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("mouse" "visits" "bear" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The mouse does not see the mouse.
True
4
proof
[(((((((triple1) -> rule5)) -> rule3)) -> rule2))]
("mouse" "sees" "mouse" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
The mouse sees the mouse.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule3)) -> rule2))]
("mouse" "sees" "mouse" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
The cow does not visit the mouse.
Unknown
inv-random
[@0: The cow visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "mouse" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bear visits the dog.[(triple1)] The cow does not see the dog.[(triple4)] The cow is big.[(triple2)] The cow sees the bear.[(triple3)] The dog sees the bear.[(triple5)] The mouse is big.[(triple6)] The mouse sees the cow.[(triple7)] @1: The cow visits the bear.[(((triple7) -> rule1))] The dog sees the mouse.[(((triple1) -> rule5))] @2: The cow does not see the mouse.[(((((triple7) -> rule1)) -> rule2))] The mouse visits the bear.[(((((triple1) -> rule5)) -> rule3))] @3: The mouse does not see the mouse.[(((((((triple1) -> rule5)) -> rule3)) -> rule2))]
The bear visits the dog.
("bear" "visits" "dog" "+")
triple1
The cow does not see the dog.
("cow" "sees" "dog" "-")
triple4
The cow is big.
("cow" "is" "big" "+")
triple2
The cow sees the bear.
("cow" "sees" "bear" "+")
triple3
The dog sees the bear.
("dog" "sees" "bear" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple7
The cow visits the bear.
("cow" "visits" "bear" "+")
((triple7) -> (rule1 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((triple1) -> (rule5 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3