The bear sees the rabbit. The cow does not visit the rabbit. The rabbit sees the cow. If something sees the cow and it is cold then it is rough. If something eats the rabbit then the rabbit does not visit the bear. If the rabbit sees the cow then the cow visits the bear. If something sees the cow then it eats the rabbit. If something is rough and it does not eat the cow then it does not visit the bear. If something visits the bear then the bear sees the cow.
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If something sees the cow and it is cold then it is rough.
((("something" "sees" "cow" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something eats the rabbit then the rabbit does not visit the bear.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "visits" "bear" "-"))
If the rabbit sees the cow then the cow visits the bear.
((("rabbit" "sees" "cow" "+")) -> ("cow" "visits" "bear" "+"))
If something sees the cow then it eats the rabbit.
((("something" "sees" "cow" "+")) -> ("something" "eats" "rabbit" "+"))
If something is rough and it does not eat the cow then it does not visit the bear.
((("something" "is" "rough" "+") ("something" "eats" "cow" "~")) -> ("something" "visits" "bear" "-"))
If something visits the bear then the bear sees the cow.
((("something" "visits" "bear" "+")) -> ("bear" "sees" "cow" "+"))
The cow does not visit the rabbit.
True
1
proof
[(triple2)]
("cow" "visits" "rabbit" "-")
triple2
The cow visits the rabbit.
False
1
inv-proof
[(triple2)]
("cow" "visits" "rabbit" "+")
triple2
The rabbit eats the rabbit.
True
2
proof
[(((triple3) -> rule4))]
("rabbit" "eats" "rabbit" "+")
((triple3) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The cow does not visit the bear.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "visits" "bear" "-")
((triple3) -> (rule3 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The rabbit does not visit the bear.
True
3
proof
[(((((triple3) -> rule4)) -> rule2) OR ((((((((triple3) -> rule3)) -> rule6)) -> rule4)) -> rule2))]
("rabbit" "visits" "bear" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((((((triple3) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
The bear sees the cow.
("bear" "sees" "cow" "+")
int3
The cow visits the bear.
("cow" "visits" "bear" "+")
int4
The bear does not see the cow.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("bear" "sees" "cow" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The bear eats the rabbit.
True
4
proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule4))]
("bear" "eats" "rabbit" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2
The cow visits the bear.
("cow" "visits" "bear" "+")
int3
The bear does not eat the rabbit.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule4))]
("bear" "eats" "rabbit" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2
The cow visits the bear.
("cow" "visits" "bear" "+")
int3
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "rough" "-")
The bear is rough.
Unknown
rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "rough" "+")
The cow does not eat the rabbit.
Unknown
inv-rconc
[@1: The cow eats the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "rabbit" "-")
The cow is rough.
Unknown
rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "rough" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
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 cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The bear sees the rabbit.[(triple1)] The cow does not visit the rabbit.[(triple2)] The rabbit sees the cow.[(triple3)] @1: The cow visits the bear.[(((triple3) -> rule3))] The rabbit eats the rabbit.[(((triple3) -> rule4))] @2: The bear sees the cow.[(((((triple3) -> rule3)) -> rule6))] The rabbit does not visit the bear.[(((((triple3) -> rule4)) -> rule2) OR ((((((((triple3) -> rule3)) -> rule6)) -> rule4)) -> rule2))] @3: The bear eats the rabbit.[(((((((triple3) -> rule3)) -> rule6)) -> rule4))]
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple1
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
triple2
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple3
The cow visits the bear.
("cow" "visits" "bear" "+")
((triple3) -> (rule3 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple3) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((((((triple3) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
The bear sees the cow.
("bear" "sees" "cow" "+")
int3
The cow visits the bear.
("cow" "visits" "bear" "+")
int4
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2
The cow visits the bear.
("cow" "visits" "bear" "+")
int3