The cow sees the dog. The cow sees the mouse. The dog is kind. The dog does not see the mouse. The dog visits the cow. The dog visits the mouse. The mouse is nice. The mouse likes the cow. The mouse sees the dog. The mouse visits the cow. If something visits the cow then the cow sees the mouse. If something visits the dog and it visits the cow then it visits the mouse. If the dog does not like the mouse then the mouse does not visit the dog. If something sees the dog then it sees the cow. If something sees the cow then the cow likes the mouse. If something sees the mouse then the mouse sees the dog.
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
The dog visits the cow.
("dog" "visits" "cow" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something visits the cow then the cow sees the mouse.
((("something" "visits" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If something visits the dog and it visits the cow then it visits the mouse.
((("something" "visits" "dog" "+") ("something" "visits" "cow" "+")) -> ("something" "visits" "mouse" "+"))
If the dog does not like the mouse then the mouse does not visit the dog.
((("dog" "likes" "mouse" "~")) -> ("mouse" "visits" "dog" "-"))
If something sees the dog then it sees the cow.
((("something" "sees" "dog" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cow then the cow likes the mouse.
((("something" "sees" "cow" "+")) -> ("cow" "likes" "mouse" "+"))
If something sees the mouse then the mouse sees the dog.
((("something" "sees" "mouse" "+")) -> ("mouse" "sees" "dog" "+"))
The dog is kind.
True
1
proof
[(triple3)]
("dog" "is" "kind" "+")
triple3
The mouse is not nice.
False
1
inv-proof
[(triple7)]
("mouse" "is" "nice" "-")
triple7
The mouse sees the cow.
True
2
proof
[(((triple9) -> rule4) OR ((((triple2) -> rule6)) -> rule4) OR ((((((triple10) -> rule1)) -> rule6)) -> rule4) OR ((((((triple5) -> rule1)) -> rule6)) -> rule4))]
("mouse" "sees" "cow" "+")
((triple9) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
((((((triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The mouse does not see the cow.
False
2
inv-proof
[(((triple9) -> rule4) OR ((((triple2) -> rule6)) -> rule4) OR ((((((triple10) -> rule1)) -> rule6)) -> rule4) OR ((((((triple5) -> rule1)) -> rule6)) -> rule4))]
("mouse" "sees" "cow" "-")
((triple9) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
((((((triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The cow likes the mouse.
True
3
proof
[(((((triple1) -> rule4)) -> rule5) OR ((((triple9) -> rule4)) -> rule5) OR ((((((triple2) -> rule6)) -> rule4)) -> rule5) OR ((((((((triple10) -> rule1)) -> rule6)) -> rule4)) -> rule5) OR ((((((((triple5) -> rule1)) -> rule6)) -> rule4)) -> rule5))]
("cow" "likes" "mouse" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
((((((((triple10) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int4
((((((((triple5) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int4
The cow does not like the mouse.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5) OR ((((triple9) -> rule4)) -> rule5) OR ((((((triple2) -> rule6)) -> rule4)) -> rule5) OR ((((((((triple10) -> rule1)) -> rule6)) -> rule4)) -> rule5) OR ((((((((triple5) -> rule1)) -> rule6)) -> rule4)) -> rule5))]
("cow" "likes" "mouse" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
((((((((triple10) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int4
((((((((triple5) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int4
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The dog sees the cow.
Unknown
rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "sees" "cow" "+")
The cow does not visit the mouse.
Unknown
inv-rconc
[@1: The cow visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "mouse" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The cow sees the dog.[(triple1)] The cow sees the mouse.[(triple2 OR ((triple10) -> rule1) OR ((triple5) -> rule1))] The dog does not see the mouse.[(triple4)] The dog is kind.[(triple3)] The dog visits the cow.[(triple5)] The dog visits the mouse.[(triple6)] The mouse is nice.[(triple7)] The mouse likes the cow.[(triple8)] The mouse sees the dog.[(triple9 OR ((triple2) -> rule6) OR ((((triple10) -> rule1)) -> rule6) OR ((((triple5) -> rule1)) -> rule6))] The mouse visits the cow.[(triple10)] @1: The cow sees the cow.[(((triple1) -> rule4))] The mouse sees the cow.[(((triple9) -> rule4) OR ((((triple2) -> rule6)) -> rule4) OR ((((((triple10) -> rule1)) -> rule6)) -> rule4) OR ((((((triple5) -> rule1)) -> rule6)) -> rule4))] @2: The cow likes the mouse.[(((((triple1) -> rule4)) -> rule5) OR ((((triple9) -> rule4)) -> rule5) OR ((((((triple2) -> rule6)) -> rule4)) -> rule5) OR ((((((((triple10) -> rule1)) -> rule6)) -> rule4)) -> rule5) OR ((((((((triple5) -> rule1)) -> rule6)) -> rule4)) -> rule5))]
The cow sees the dog.
("cow" "sees" "dog" "+")
triple1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple2
((triple10) -> (rule1 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
((triple5) -> (rule1 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog visits the cow.
("dog" "visits" "cow" "+")
triple5
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple6
The mouse is nice.
("mouse" "is" "nice" "+")
triple7
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple8
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple9
((triple2) -> (rule6 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple10
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple1) -> (rule4 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((triple9) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
((((((triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
((((((((triple10) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int4
((((((((triple5) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int4