The cow eats the rabbit. The rabbit sees the cow. If the cow sees the rabbit then the rabbit is rough. If something is rough then it eats the rabbit. If something is rough then it eats the rabbit. If something eats the rabbit then it is young. If something eats the cow then the cow does not eat the rabbit. If something chases the cow and it does not chase the rabbit then the cow eats the rabbit. If the cow eats the rabbit then the cow sees the rabbit. If the rabbit sees the cow then the rabbit chases the cow.
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If the cow sees the rabbit then the rabbit is rough.
((("cow" "sees" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If something is rough then it eats the rabbit.
((("something" "is" "rough" "+")) -> ("something" "eats" "rabbit" "+"))
If something is rough then it eats the rabbit.
((("something" "is" "rough" "+")) -> ("something" "eats" "rabbit" "+"))
If something eats the rabbit then it is young.
((("something" "eats" "rabbit" "+")) -> ("something" "is" "young" "+"))
If something eats the cow then the cow does not eat the rabbit.
((("something" "eats" "cow" "+")) -> ("cow" "eats" "rabbit" "-"))
If something chases the cow and it does not chase the rabbit then the cow eats the rabbit.
((("something" "chases" "cow" "+") ("something" "chases" "rabbit" "~")) -> ("cow" "eats" "rabbit" "+"))
If the cow eats the rabbit then the cow sees the rabbit.
((("cow" "eats" "rabbit" "+")) -> ("cow" "sees" "rabbit" "+"))
If the rabbit sees the cow then the rabbit chases the cow.
((("rabbit" "sees" "cow" "+")) -> ("rabbit" "chases" "cow" "+"))
The cow eats the rabbit.
True
1
proof
[(triple1)]
("cow" "eats" "rabbit" "+")
triple1
The cow does not eat the rabbit.
False
1
inv-proof
[(triple1)]
("cow" "eats" "rabbit" "-")
triple1
The cow is young.
True
2
proof
[(((triple1) -> rule4))]
("cow" "is" "young" "+")
((triple1) -> (rule4 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The rabbit does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule8))]
("rabbit" "chases" "cow" "-")
((triple2) -> (rule8 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit is rough.
True
3
proof
[(((((triple1) -> rule7)) -> rule1))]
("rabbit" "is" "rough" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The rabbit is not rough.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule1))]
("rabbit" "is" "rough" "-")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The rabbit eats the rabbit.
True
4
proof
[(((((((triple1) -> rule7)) -> rule1)) -> rule2) OR ((((((triple1) -> rule7)) -> rule1)) -> rule3))]
("rabbit" "eats" "rabbit" "+")
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The rabbit does not eat the rabbit.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule1)) -> rule2) OR ((((((triple1) -> rule7)) -> rule1)) -> rule3))]
("rabbit" "eats" "rabbit" "-")
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The rabbit does not eat the cow.
Unknown
inv-random
[@0: The rabbit eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cow" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow eats the rabbit.[(triple1)] The rabbit sees the cow.[(triple2)] @1: The cow is young.[(((triple1) -> rule4))] The cow sees the rabbit.[(((triple1) -> rule7))] The rabbit chases the cow.[(((triple2) -> rule8))] @2: The rabbit is rough.[(((((triple1) -> rule7)) -> rule1))] @3: The rabbit eats the rabbit.[(((((((triple1) -> rule7)) -> rule1)) -> rule2) OR ((((((triple1) -> rule7)) -> rule1)) -> rule3))] @4: The rabbit is young.[(((((((((triple1) -> rule7)) -> rule1)) -> rule2)) -> rule4) OR ((((((((triple1) -> rule7)) -> rule1)) -> rule3)) -> rule4))]
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple2
The cow is young.
("cow" "is" "young" "+")
((triple1) -> (rule4 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((triple1) -> (rule7 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((triple2) -> (rule8 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
((((((((triple1) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4