The bear eats the cow. The cow is big. The cow visits the rabbit. The lion is big. The rabbit eats the lion. The rabbit is big. The rabbit is nice. If someone is big and they eat the rabbit then the rabbit visits the bear. If someone visits the lion then they are blue. If someone eats the bear then they chase the rabbit. If the bear eats the lion and the lion visits the cow then the lion chases the bear. If someone is rough then they visit the lion. If someone chases the cow then they chase the rabbit. If someone visits the rabbit then they are nice. If the rabbit is nice then the rabbit is rough.
The bear eats the cow.
("bear" "eats" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
If someone is big and they eat the rabbit then the rabbit visits the bear.
((("someone" "is" "big" "+") ("someone" "eats" "rabbit" "+")) -> ("rabbit" "visits" "bear" "+"))
If someone visits the lion then they are blue.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "blue" "+"))
If someone eats the bear then they chase the rabbit.
((("someone" "eats" "bear" "+")) -> ("someone" "chases" "rabbit" "+"))
If the bear eats the lion and the lion visits the cow then the lion chases the bear.
((("bear" "eats" "lion" "+") ("lion" "visits" "cow" "+")) -> ("lion" "chases" "bear" "+"))
If someone is rough then they visit the lion.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "lion" "+"))
If someone chases the cow then they chase the rabbit.
((("someone" "chases" "cow" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone visits the rabbit then they are nice.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "nice" "+"))
If the rabbit is nice then the rabbit is rough.
((("rabbit" "is" "nice" "+")) -> ("rabbit" "is" "rough" "+"))
The cow is big.
True
1
proof
[(triple2)]
("cow" "is" "big" "+")
triple2
The cow is not big.
False
1
inv-proof
[(triple2)]
("cow" "is" "big" "-")
triple2
The rabbit is rough.
True
2
proof
[(((triple7) -> rule8))]
("rabbit" "is" "rough" "+")
((triple7) -> (rule8 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple3) -> rule7))]
("cow" "is" "nice" "-")
((triple3) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The rabbit visits the lion.
True
3
proof
[(((((triple7) -> rule8)) -> rule5))]
("rabbit" "visits" "lion" "+")
((((triple7) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit does not visit the lion.
False
3
inv-proof
[(((((triple7) -> rule8)) -> rule5))]
("rabbit" "visits" "lion" "-")
((((triple7) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is blue.
True
4
proof
[(((((((triple7) -> rule8)) -> rule5)) -> rule2))]
("rabbit" "is" "blue" "+")
((((((triple7) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The rabbit is not blue.
False
4
inv-proof
[(((((((triple7) -> rule8)) -> rule5)) -> rule2))]
("rabbit" "is" "blue" "-")
((((((triple7) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The lion does not chase the bear.
Unknown
inv-rconc
[@1: The lion chases the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "chases" "bear" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The cow is not blue.
Unknown
inv-rconc
[@2: The cow is blue.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("cow" "is" "blue" "-")
The lion is blue.
Unknown
rconc
[@2: The lion is blue.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("lion" "is" "blue" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The rabbit chases the bear.
Unknown
random
[@0: The rabbit chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "bear" "+")
@0: The bear eats the cow.[(triple1)] The cow is big.[(triple2)] The cow visits the rabbit.[(triple3)] The lion is big.[(triple4)] The rabbit eats the lion.[(triple5)] The rabbit is big.[(triple6)] The rabbit is nice.[(triple7)] @1: The cow is nice.[(((triple3) -> rule7))] The rabbit is rough.[(((triple7) -> rule8))] @2: The rabbit visits the lion.[(((((triple7) -> rule8)) -> rule5))] @3: The rabbit is blue.[(((((((triple7) -> rule8)) -> rule5)) -> rule2))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple3
The lion is big.
("lion" "is" "big" "+")
triple4
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple5
The rabbit is big.
("rabbit" "is" "big" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The cow is nice.
("cow" "is" "nice" "+")
((triple3) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple7) -> (rule8 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
((((triple7) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((((triple7) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3