The bear is round. The bear sees the cow. The cow eats the bear. The cow is big. The cow is cold. The cow likes the bear. The rabbit eats the bear. The rabbit eats the cow. The rabbit is nice. The rabbit is rough. The rabbit is round. The rabbit likes the bear. The rabbit likes the cow. The rabbit sees the bear. The rabbit sees the cow. If something sees the cow and it is big then the cow likes the rabbit. If something sees the bear and the bear sees the cow then the cow sees the bear. If something sees the cow then the cow eats the bear. If something likes the bear then it eats the rabbit. If something sees the rabbit then it eats the bear. If something eats the cow and it likes the cow then it eats the rabbit. If something is nice and it eats the rabbit then it is big. If something is rough and it eats the cow then the cow likes the bear.
The bear is round.
("bear" "is" "round" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If something sees the cow and it is big then the cow likes the rabbit.
((("something" "sees" "cow" "+") ("something" "is" "big" "+")) -> ("cow" "likes" "rabbit" "+"))
If something sees the bear and the bear sees the cow then the cow sees the bear.
((("something" "sees" "bear" "+") ("bear" "sees" "cow" "+")) -> ("cow" "sees" "bear" "+"))
If something sees the cow then the cow eats the bear.
((("something" "sees" "cow" "+")) -> ("cow" "eats" "bear" "+"))
If something likes the bear then it eats the rabbit.
((("something" "likes" "bear" "+")) -> ("something" "eats" "rabbit" "+"))
If something sees the rabbit then it eats the bear.
((("something" "sees" "rabbit" "+")) -> ("something" "eats" "bear" "+"))
If something eats the cow and it likes the cow then it eats the rabbit.
((("something" "eats" "cow" "+") ("something" "likes" "cow" "+")) -> ("something" "eats" "rabbit" "+"))
If something is nice and it eats the rabbit then it is big.
((("something" "is" "nice" "+") ("something" "eats" "rabbit" "+")) -> ("something" "is" "big" "+"))
If something is rough and it eats the cow then the cow likes the bear.
((("something" "is" "rough" "+") ("something" "eats" "cow" "+")) -> ("cow" "likes" "bear" "+"))
The rabbit sees the bear.
True
1
proof
[(triple14)]
("rabbit" "sees" "bear" "+")
triple14
The rabbit does not like the bear.
False
1
inv-proof
[(triple12)]
("rabbit" "likes" "bear" "-")
triple12
The cow eats the rabbit.
True
2
proof
[(((triple6) -> rule4) OR ((((triple10 triple8) -> rule8)) -> rule4))]
("cow" "eats" "rabbit" "+")
((triple6) -> (rule4 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
((((triple10 triple8) -> (rule8 % int2))) -> (rule4 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The cow does not see the bear.
False
3
inv-proof
[(((triple14 triple2) -> rule2))]
("cow" "sees" "bear" "-")
((triple14 triple2) -> (rule2 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The rabbit is big.
True
4
proof
[(((triple9 ((triple12) -> rule4)) -> rule7) OR ((triple9 ((triple8 triple13) -> rule6)) -> rule7))]
("rabbit" "is" "big" "+")
((triple9 ((triple12) -> (rule4 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((triple9 ((triple8 triple13) -> (rule6 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit is not big.
False
4
inv-proof
[(((triple9 ((triple12) -> rule4)) -> rule7) OR ((triple9 ((triple8 triple13) -> rule6)) -> rule7))]
("rabbit" "is" "big" "-")
((triple9 ((triple12) -> (rule4 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((triple9 ((triple8 triple13) -> (rule6 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The cow likes the rabbit.
True
6
proof
[(((triple15 ((triple9 ((triple12) -> rule4)) -> rule7)) -> rule1) OR ((triple15 ((triple9 ((triple8 triple13) -> rule6)) -> rule7)) -> rule1))]
("cow" "likes" "rabbit" "+")
((triple15 ((triple9 ((triple12) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
((triple15 ((triple9 ((triple8 triple13) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
The cow does not like the rabbit.
False
6
inv-proof
[(((triple15 ((triple9 ((triple12) -> rule4)) -> rule7)) -> rule1) OR ((triple15 ((triple9 ((triple8 triple13) -> rule6)) -> rule7)) -> rule1))]
("cow" "likes" "rabbit" "-")
((triple15 ((triple9 ((triple12) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
((triple15 ((triple9 ((triple8 triple13) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "bear" "-")
The bear eats the rabbit.
Unknown
rconc
[@1: The bear eats the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "eats" "rabbit" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "big" "-")
The bear sees the rabbit.
Unknown
random
[@0: The bear sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "rabbit" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The bear likes the cow.
Unknown
random
[@0: The bear likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cow" "+")
@0: The bear is round.[(triple1)] The bear sees the cow.[(triple2)] The cow eats the bear.[(triple3 OR ((triple15) -> rule3) OR ((triple2) -> rule3))] The cow is big.[(triple4)] The cow is cold.[(triple5)] The cow likes the bear.[(triple6 OR ((triple10 triple8) -> rule8))] The rabbit eats the bear.[(triple7)] The rabbit eats the cow.[(triple8)] The rabbit is nice.[(triple9)] The rabbit is rough.[(triple10)] The rabbit is round.[(triple11)] The rabbit likes the bear.[(triple12)] The rabbit likes the cow.[(triple13)] The rabbit sees the bear.[(triple14)] The rabbit sees the cow.[(triple15)] @1: The cow eats the rabbit.[(((triple6) -> rule4) OR ((((triple10 triple8) -> rule8)) -> rule4))] The cow sees the bear.[(((triple14 triple2) -> rule2))] The rabbit eats the rabbit.[(((triple12) -> rule4) OR ((triple8 triple13) -> rule6))] @2: The rabbit is big.[(((triple9 ((triple12) -> rule4)) -> rule7) OR ((triple9 ((triple8 triple13) -> rule6)) -> rule7))] @3: The cow likes the rabbit.[(((triple15 ((triple9 ((triple12) -> rule4)) -> rule7)) -> rule1) OR ((triple15 ((triple9 ((triple8 triple13) -> rule6)) -> rule7)) -> rule1))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear sees the cow.
("bear" "sees" "cow" "+")
triple2
The cow eats the bear.
("cow" "eats" "bear" "+")
triple3
((triple15) -> (rule3 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
((triple2) -> (rule3 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow is big.
("cow" "is" "big" "+")
triple4
The cow is cold.
("cow" "is" "cold" "+")
triple5
The cow likes the bear.
("cow" "likes" "bear" "+")
triple6
((triple10 triple8) -> (rule8 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple7
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple8
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple9
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple12
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple13
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple14
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple15
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
((triple6) -> (rule4 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
((((triple10 triple8) -> (rule8 % int2))) -> (rule4 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The cow sees the bear.
("cow" "sees" "bear" "+")
((triple14 triple2) -> (rule2 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple12) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((triple8 triple13) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple9 ((triple12) -> (rule4 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((triple9 ((triple8 triple13) -> (rule6 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
((triple15 ((triple9 ((triple12) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
((triple15 ((triple9 ((triple8 triple13) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3