The cow eats the rabbit. The cow is green. The cow likes the rabbit. The cow needs the rabbit. The rabbit eats the cow. The rabbit is big. The rabbit is blue. The rabbit is green. The rabbit is kind. The rabbit is rough. The rabbit likes the cow. The rabbit needs the cow. If the cow needs the rabbit and the cow likes the rabbit then the rabbit needs the cow. If something eats the cow then it is big. If something is blue and it eats the cow then it eats the rabbit. If the rabbit likes the cow then the rabbit eats the cow. If something is big then it needs the rabbit. If something needs the cow and it is big then the cow needs the rabbit.
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is green.
("cow" "is" "green" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If the cow needs the rabbit and the cow likes the rabbit then the rabbit needs the cow.
((("cow" "needs" "rabbit" "+") ("cow" "likes" "rabbit" "+")) -> ("rabbit" "needs" "cow" "+"))
If something eats the cow then it is big.
((("something" "eats" "cow" "+")) -> ("something" "is" "big" "+"))
If something is blue and it eats the cow then it eats the rabbit.
((("something" "is" "blue" "+") ("something" "eats" "cow" "+")) -> ("something" "eats" "rabbit" "+"))
If the rabbit likes the cow then the rabbit eats the cow.
((("rabbit" "likes" "cow" "+")) -> ("rabbit" "eats" "cow" "+"))
If something is big then it needs the rabbit.
((("something" "is" "big" "+")) -> ("something" "needs" "rabbit" "+"))
If something needs the cow and it is big then the cow needs the rabbit.
((("something" "needs" "cow" "+") ("something" "is" "big" "+")) -> ("cow" "needs" "rabbit" "+"))
The rabbit eats the cow.
True
1
proof
[(triple5 OR ((triple11) -> rule4))]
("rabbit" "eats" "cow" "+")
triple5
((triple11) -> (rule4 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The cow does not eat the rabbit.
False
1
inv-proof
[(triple1)]
("cow" "eats" "rabbit" "-")
triple1
The rabbit needs the rabbit.
True
2
proof
[(((triple6) -> rule5) OR ((((triple5) -> rule2)) -> rule5) OR ((((((triple11) -> rule4)) -> rule2)) -> rule5))]
("rabbit" "needs" "rabbit" "+")
((triple6) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int3
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple6) -> rule5) OR ((((triple5) -> rule2)) -> rule5) OR ((((((triple11) -> rule4)) -> rule2)) -> rule5))]
("rabbit" "needs" "rabbit" "-")
((triple6) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int3
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "big" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cow eats the rabbit.[(triple1)] The cow is green.[(triple2)] The cow likes the rabbit.[(triple3)] The cow needs the rabbit.[(triple4 OR ((triple12 triple6) -> rule6) OR ((triple12 ((triple5) -> rule2)) -> rule6) OR ((triple12 ((((triple11) -> rule4)) -> rule2)) -> rule6))] The rabbit eats the cow.[(triple5 OR ((triple11) -> rule4))] The rabbit is big.[(triple6 OR ((triple5) -> rule2) OR ((((triple11) -> rule4)) -> rule2))] The rabbit is blue.[(triple7)] The rabbit is green.[(triple8)] The rabbit is kind.[(triple9)] The rabbit is rough.[(triple10)] The rabbit likes the cow.[(triple11)] The rabbit needs the cow.[(triple12 OR ((triple4 triple3) -> rule1))] @1: The rabbit eats the rabbit.[(((triple7 triple5) -> rule3) OR ((triple7 ((triple11) -> rule4)) -> rule3))] The rabbit needs the rabbit.[(((triple6) -> rule5) OR ((((triple5) -> rule2)) -> rule5) OR ((((((triple11) -> rule4)) -> rule2)) -> rule5))]
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple3
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple4
((triple12 triple6) -> (rule6 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
((triple12 ((triple5) -> (rule2 % int2))) -> (rule6 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((triple12 ((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int3
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple5
((triple11) -> (rule4 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple6
((triple5) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((((triple11) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple7
The rabbit is green.
("rabbit" "is" "green" "+")
triple8
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple9
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple10
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple11
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple12
((triple4 triple3) -> (rule1 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple7 triple5) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((triple7 ((triple11) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple6) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((((((triple11) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int3