The bear chases the squirrel. The bear is big. The cow is green. The cow is young. The rabbit is nice. The rabbit sees the bear. The squirrel is green. If someone visits the bear then they visit the rabbit. If someone is nice then they visit the bear. If someone chases the rabbit and they see the bear then the rabbit visits the squirrel. If someone visits the rabbit then they are green. If someone sees the bear then they visit the bear. If someone chases the cow then they are round. If the cow chases the bear then the bear visits the rabbit. If someone is green then they visit the cow. If someone is nice and they visit the cow then they chase the squirrel.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is big.
("bear" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is young.
("cow" "is" "young" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
If someone visits the bear then they visit the rabbit.
((("someone" "visits" "bear" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is nice then they visit the bear.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "bear" "+"))
If someone chases the rabbit and they see the bear then the rabbit visits the squirrel.
((("someone" "chases" "rabbit" "+") ("someone" "sees" "bear" "+")) -> ("rabbit" "visits" "squirrel" "+"))
If someone visits the rabbit then they are green.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "green" "+"))
If someone sees the bear then they visit the bear.
((("someone" "sees" "bear" "+")) -> ("someone" "visits" "bear" "+"))
If someone chases the cow then they are round.
((("someone" "chases" "cow" "+")) -> ("someone" "is" "round" "+"))
If the cow chases the bear then the bear visits the rabbit.
((("cow" "chases" "bear" "+")) -> ("bear" "visits" "rabbit" "+"))
If someone is green then they visit the cow.
((("someone" "is" "green" "+")) -> ("someone" "visits" "cow" "+"))
If someone is nice and they visit the cow then they chase the squirrel.
((("someone" "is" "nice" "+") ("someone" "visits" "cow" "+")) -> ("someone" "chases" "squirrel" "+"))
The rabbit sees the bear.
True
1
proof
[(triple6)]
("rabbit" "sees" "bear" "+")
triple6
The cow is not young.
False
1
inv-proof
[(triple4)]
("cow" "is" "young" "-")
triple4
The squirrel visits the cow.
True
2
proof
[(((triple7) -> rule8))]
("squirrel" "visits" "cow" "+")
((triple7) -> (rule8 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple3) -> rule8))]
("cow" "visits" "cow" "-")
((triple3) -> (rule8 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The rabbit visits the rabbit.
True
3
proof
[(((((triple5) -> rule2)) -> rule1) OR ((((triple6) -> rule5)) -> rule1))]
("rabbit" "visits" "rabbit" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The rabbit does not visit the rabbit.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule1) OR ((((triple6) -> rule5)) -> rule1))]
("rabbit" "visits" "rabbit" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The rabbit is green.
True
4
proof
[(((((((triple5) -> rule2)) -> rule1)) -> rule4) OR ((((((triple6) -> rule5)) -> rule1)) -> rule4))]
("rabbit" "is" "green" "+")
((((((triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int3
The rabbit is not green.
False
4
inv-proof
[(((((((triple5) -> rule2)) -> rule1)) -> rule4) OR ((((((triple6) -> rule5)) -> rule1)) -> rule4))]
("rabbit" "is" "green" "-")
((((((triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int3
The rabbit visits the cow.
True
5
proof
[(((((((((triple5) -> rule2)) -> rule1)) -> rule4)) -> rule8) OR ((((((((triple6) -> rule5)) -> rule1)) -> rule4)) -> rule8))]
("rabbit" "visits" "cow" "+")
((((((((triple5) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int4
The rabbit does not visit the cow.
False
5
inv-proof
[(((((((((triple5) -> rule2)) -> rule1)) -> rule4)) -> rule8) OR ((((((((triple6) -> rule5)) -> rule1)) -> rule4)) -> rule8))]
("rabbit" "visits" "cow" "-")
((((((((triple5) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int4
The rabbit chases the squirrel.
True
7
proof
[(((triple5 ((((((((triple5) -> rule2)) -> rule1)) -> rule4)) -> rule8)) -> rule9) OR ((triple5 ((((((((triple6) -> rule5)) -> rule1)) -> rule4)) -> rule8)) -> rule9))]
("rabbit" "chases" "squirrel" "+")
((triple5 ((((((((triple5) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int4
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int5
((triple5 ((((((((triple6) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int4
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int5
The rabbit does not chase the squirrel.
False
7
inv-proof
[(((triple5 ((((((((triple5) -> rule2)) -> rule1)) -> rule4)) -> rule8)) -> rule9) OR ((triple5 ((((((((triple6) -> rule5)) -> rule1)) -> rule4)) -> rule8)) -> rule9))]
("rabbit" "chases" "squirrel" "-")
((triple5 ((((((((triple5) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int4
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int5
((triple5 ((((((((triple6) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int4
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int5
The squirrel does not visit the rabbit.
Unknown
inv-rconc
[@2: The squirrel visits the rabbit.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("squirrel" "visits" "rabbit" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "round" "-")
The rabbit is round.
Unknown
rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "round" "+")
The cow does not chase the squirrel.
Unknown
inv-rconc
[@1: The cow chases the squirrel.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cow" "chases" "squirrel" "-")
The bear visits the bear.
Unknown
rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "visits" "bear" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The squirrel chases the rabbit.
Unknown
random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "+")
The rabbit does not see the squirrel.
Unknown
inv-random
[@0: The rabbit sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "squirrel" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
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 chases the squirrel.[(triple1)] The bear is big.[(triple2)] The cow is green.[(triple3)] The cow is young.[(triple4)] The rabbit is nice.[(triple5)] The rabbit sees the bear.[(triple6)] The squirrel is green.[(triple7)] @1: The cow visits the cow.[(((triple3) -> rule8))] The rabbit visits the bear.[(((triple5) -> rule2) OR ((triple6) -> rule5))] The squirrel visits the cow.[(((triple7) -> rule8))] @2: The rabbit visits the rabbit.[(((((triple5) -> rule2)) -> rule1) OR ((((triple6) -> rule5)) -> rule1))] @3: The rabbit is green.[(((((((triple5) -> rule2)) -> rule1)) -> rule4) OR ((((((triple6) -> rule5)) -> rule1)) -> rule4))] @4: The rabbit visits the cow.[(((((((((triple5) -> rule2)) -> rule1)) -> rule4)) -> rule8) OR ((((((((triple6) -> rule5)) -> rule1)) -> rule4)) -> rule8))] @5: The rabbit chases the squirrel.[(((triple5 ((((((((triple5) -> rule2)) -> rule1)) -> rule4)) -> rule8)) -> rule9) OR ((triple5 ((((((((triple6) -> rule5)) -> rule1)) -> rule4)) -> rule8)) -> rule9))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple5
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple6
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple3) -> (rule8 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
((triple5) -> (rule2 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
((triple6) -> (rule5 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
((triple7) -> (rule8 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
((((((triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int3
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
((((((((triple5) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int4
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
((triple5 ((((((((triple5) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int4
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int5
((triple5 ((((((((triple6) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int4
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int5