The bear likes the rabbit. The bear visits the mouse. The cow does not chase the bear. The cow is round. The cow likes the bear. The mouse does not chase the rabbit. The mouse is blue. The mouse is green. The mouse is rough. The mouse likes the bear. The mouse likes the cow. The rabbit does not chase the mouse. The rabbit is big. The rabbit does not like the mouse. The rabbit visits the cow. If someone visits the bear then the bear chases the mouse. If someone likes the rabbit and the rabbit visits the bear then they do not like the bear. If someone chases the mouse then the mouse visits the rabbit. If the bear visits the rabbit and the rabbit visits the cow then the cow does not like the mouse. If someone likes the bear then they visit the bear. If someone is green and they visit the rabbit then they do not chase the rabbit. If someone chases the rabbit then they chase the bear. If someone is round and they do not like the mouse then they do not chase the bear.
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cow does not chase the bear.
("cow" "chases" "bear" "-")
The cow is round.
("cow" "is" "round" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If someone visits the bear then the bear chases the mouse.
((("someone" "visits" "bear" "+")) -> ("bear" "chases" "mouse" "+"))
If someone likes the rabbit and the rabbit visits the bear then they do not like the bear.
((("someone" "likes" "rabbit" "+") ("rabbit" "visits" "bear" "+")) -> ("someone" "likes" "bear" "-"))
If someone chases the mouse then the mouse visits the rabbit.
((("someone" "chases" "mouse" "+")) -> ("mouse" "visits" "rabbit" "+"))
If the bear visits the rabbit and the rabbit visits the cow then the cow does not like the mouse.
((("bear" "visits" "rabbit" "+") ("rabbit" "visits" "cow" "+")) -> ("cow" "likes" "mouse" "-"))
If someone likes the bear then they visit the bear.
((("someone" "likes" "bear" "+")) -> ("someone" "visits" "bear" "+"))
If someone is green and they visit the rabbit then they do not chase the rabbit.
((("someone" "is" "green" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "chases" "rabbit" "-"))
If someone chases the rabbit then they chase the bear.
((("someone" "chases" "rabbit" "+")) -> ("someone" "chases" "bear" "+"))
If someone is round and they do not like the mouse then they do not chase the bear.
((("someone" "is" "round" "+") ("someone" "likes" "mouse" "~")) -> ("someone" "chases" "bear" "-"))
The mouse is blue.
True
1
proof
[(triple7)]
("mouse" "is" "blue" "+")
triple7
The mouse is not blue.
False
1
inv-proof
[(triple7)]
("mouse" "is" "blue" "-")
triple7
The mouse visits the bear.
True
2
proof
[(((triple10) -> rule5))]
("mouse" "visits" "bear" "+")
((triple10) -> (rule5 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The cow does not visit the bear.
False
2
inv-proof
[(((triple5) -> rule5))]
("cow" "visits" "bear" "-")
((triple5) -> (rule5 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The bear chases the mouse.
True
3
proof
[(((((triple10) -> rule5)) -> rule1) OR ((((triple5) -> rule5)) -> rule1))]
("bear" "chases" "mouse" "+")
((((triple10) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The bear does not chase the mouse.
False
3
inv-proof
[(((((triple10) -> rule5)) -> rule1) OR ((((triple5) -> rule5)) -> rule1))]
("bear" "chases" "mouse" "-")
((((triple10) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The mouse visits the rabbit.
True
4
proof
[(((((((triple10) -> rule5)) -> rule1)) -> rule3) OR ((((((triple5) -> rule5)) -> rule1)) -> rule3))]
("mouse" "visits" "rabbit" "+")
((((((triple10) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The cow visits the bear.
("cow" "visits" "bear" "+")
int3
The mouse does not visit the rabbit.
False
4
inv-proof
[(((((((triple10) -> rule5)) -> rule1)) -> rule3) OR ((((((triple5) -> rule5)) -> rule1)) -> rule3))]
("mouse" "visits" "rabbit" "-")
((((((triple10) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The cow visits the bear.
("cow" "visits" "bear" "+")
int3
The rabbit does not visit the bear.
Unknown
inv-rconc
[@1: The rabbit visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "visits" "bear" "-")
The mouse chases the bear.
Unknown
rconc
[@1: The mouse chases the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "chases" "bear" "+")
The rabbit does not chase the bear.
Unknown
inv-rconc
[@1: The rabbit chases the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "chases" "bear" "-")
The bear visits the bear.
Unknown
rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "visits" "bear" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The bear likes the rabbit.[(triple1)] The bear visits the mouse.[(triple2)] The cow does not chase the bear.[(triple3)] The cow is round.[(triple4)] The cow likes the bear.[(triple5)] The mouse does not chase the rabbit.[(triple6 OR ((triple8 ((((((triple10) -> rule5)) -> rule1)) -> rule3)) -> rule6) OR ((triple8 ((((((triple5) -> rule5)) -> rule1)) -> rule3)) -> rule6))] The mouse is blue.[(triple7)] The mouse is green.[(triple8)] The mouse is rough.[(triple9)] The mouse likes the bear.[(triple10)] The mouse likes the cow.[(triple11)] The rabbit does not chase the mouse.[(triple12)] The rabbit does not like the mouse.[(triple14)] The rabbit is big.[(triple13)] The rabbit visits the cow.[(triple15)] @1: The cow visits the bear.[(((triple5) -> rule5))] The mouse visits the bear.[(((triple10) -> rule5))] @2: The bear chases the mouse.[(((((triple10) -> rule5)) -> rule1) OR ((((triple5) -> rule5)) -> rule1))] @3: The mouse visits the rabbit.[(((((((triple10) -> rule5)) -> rule1)) -> rule3) OR ((((((triple5) -> rule5)) -> rule1)) -> rule3))]
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple2
The cow does not chase the bear.
("cow" "chases" "bear" "-")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow likes the bear.
("cow" "likes" "bear" "+")
triple5
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
triple6
((triple8 ((((((triple10) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int4
((triple8 ((((((triple5) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The cow visits the bear.
("cow" "visits" "bear" "+")
int4
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple10
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple11
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
triple12
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
triple14
The rabbit is big.
("rabbit" "is" "big" "+")
triple13
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple15
The cow visits the bear.
("cow" "visits" "bear" "+")
((triple5) -> (rule5 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
((triple10) -> (rule5 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
((((triple10) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
((((((triple10) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The cow visits the bear.
("cow" "visits" "bear" "+")
int3