The bear is cold. The bear is young. The bear visits the dog. The dog is cold. The dog likes the mouse. The dog sees the bear. The dog visits the bear. The mouse is cold. The mouse is young. The mouse sees the bear. If the mouse sees the bear then the bear sees the mouse. If someone visits the mouse and they see the dog then they see the bear. If someone sees the dog and they visit the bear then the bear sees the dog. If someone sees the bear then the bear sees the mouse. If someone visits the dog and they see the mouse then the dog visits the mouse. If someone is kind and they visit the dog then they like the mouse. If someone is green and young then they are cold. If someone likes the bear and the bear visits the mouse then they see the dog.
The bear is cold.
("bear" "is" "cold" "+")
The bear is young.
("bear" "is" "young" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
If the mouse sees the bear then the bear sees the mouse.
((("mouse" "sees" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If someone visits the mouse and they see the dog then they see the bear.
((("someone" "visits" "mouse" "+") ("someone" "sees" "dog" "+")) -> ("someone" "sees" "bear" "+"))
If someone sees the dog and they visit the bear then the bear sees the dog.
((("someone" "sees" "dog" "+") ("someone" "visits" "bear" "+")) -> ("bear" "sees" "dog" "+"))
If someone sees the bear then the bear sees the mouse.
((("someone" "sees" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If someone visits the dog and they see the mouse then the dog visits the mouse.
((("someone" "visits" "dog" "+") ("someone" "sees" "mouse" "+")) -> ("dog" "visits" "mouse" "+"))
If someone is kind and they visit the dog then they like the mouse.
((("someone" "is" "kind" "+") ("someone" "visits" "dog" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is green and young then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone likes the bear and the bear visits the mouse then they see the dog.
((("someone" "likes" "bear" "+") ("bear" "visits" "mouse" "+")) -> ("someone" "sees" "dog" "+"))
The dog likes the mouse.
True
1
proof
[(triple5)]
("dog" "likes" "mouse" "+")
triple5
The mouse does not see the bear.
False
1
inv-proof
[(triple10)]
("mouse" "sees" "bear" "-")
triple10
The bear sees the mouse.
True
2
proof
[(((triple10) -> rule1) OR ((triple10) -> rule4) OR ((triple6) -> rule4))]
("bear" "sees" "mouse" "+")
((triple10) -> (rule1 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
((triple10) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
((triple6) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear does not see the mouse.
False
2
inv-proof
[(((triple10) -> rule1) OR ((triple10) -> rule4) OR ((triple6) -> rule4))]
("bear" "sees" "mouse" "-")
((triple10) -> (rule1 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
((triple10) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
((triple6) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The dog visits the mouse.
True
4
proof
[(((triple3 ((triple10) -> rule1)) -> rule5) OR ((triple3 ((triple10) -> rule4)) -> rule5) OR ((triple3 ((triple6) -> rule4)) -> rule5))]
("dog" "visits" "mouse" "+")
((triple3 ((triple10) -> (rule1 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
((triple3 ((triple10) -> (rule4 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
((triple3 ((triple6) -> (rule4 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The dog does not visit the mouse.
False
4
inv-proof
[(((triple3 ((triple10) -> rule1)) -> rule5) OR ((triple3 ((triple10) -> rule4)) -> rule5) OR ((triple3 ((triple6) -> rule4)) -> rule5))]
("dog" "visits" "mouse" "-")
((triple3 ((triple10) -> (rule1 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
((triple3 ((triple10) -> (rule4 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
((triple3 ((triple6) -> (rule4 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear does not see the bear.
Unknown
inv-rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "bear" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "sees" "dog" "+")
The bear does not like the mouse.
Unknown
inv-rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "likes" "mouse" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
@0: The bear is cold.[(triple1)] The bear is young.[(triple2)] The bear visits the dog.[(triple3)] The dog is cold.[(triple4)] The dog likes the mouse.[(triple5)] The dog sees the bear.[(triple6)] The dog visits the bear.[(triple7)] The mouse is cold.[(triple8)] The mouse is young.[(triple9)] The mouse sees the bear.[(triple10)] @1: The bear sees the mouse.[(((triple10) -> rule1) OR ((triple10) -> rule4) OR ((triple6) -> rule4))] @2: The dog visits the mouse.[(((triple3 ((triple10) -> rule1)) -> rule5) OR ((triple3 ((triple10) -> rule4)) -> rule5) OR ((triple3 ((triple6) -> rule4)) -> rule5))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear visits the dog.
("bear" "visits" "dog" "+")
triple3
The dog is cold.
("dog" "is" "cold" "+")
triple4
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple5
The dog sees the bear.
("dog" "sees" "bear" "+")
triple6
The dog visits the bear.
("dog" "visits" "bear" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple10
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((triple10) -> (rule1 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
((triple10) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
((triple6) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
((triple3 ((triple10) -> (rule1 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
((triple3 ((triple10) -> (rule4 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
((triple3 ((triple6) -> (rule4 % int2))) -> (rule5 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2