The bear chases the cow. The bear is nice. The bear is young. The bear visits the cow. The cow chases the bear. The cow chases the lion. The cow likes the lion. The cow visits the bear. The cow visits the lion. The lion is big. The lion visits the bear. The lion visits the cow. If the bear is big then the bear visits the lion. If the cow is kind then the cow chases the bear. If someone visits the cow then they visit the bear. If someone visits the bear then they visit the lion. If someone visits the bear then they are big. If the lion chases the cow and the lion is cold then the lion is nice.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is young.
("bear" "is" "young" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If the bear is big then the bear visits the lion.
((("bear" "is" "big" "+")) -> ("bear" "visits" "lion" "+"))
If the cow is kind then the cow chases the bear.
((("cow" "is" "kind" "+")) -> ("cow" "chases" "bear" "+"))
If someone visits the cow then they visit the bear.
((("someone" "visits" "cow" "+")) -> ("someone" "visits" "bear" "+"))
If someone visits the bear then they visit the lion.
((("someone" "visits" "bear" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the bear then they are big.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "big" "+"))
If the lion chases the cow and the lion is cold then the lion is nice.
((("lion" "chases" "cow" "+") ("lion" "is" "cold" "+")) -> ("lion" "is" "nice" "+"))
The cow visits the lion.
True
1
proof
[(triple9 OR ((triple8) -> rule4))]
("cow" "visits" "lion" "+")
triple9
((triple8) -> (rule4 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The bear does not chase the cow.
False
1
inv-proof
[(triple1)]
("bear" "chases" "cow" "-")
triple1
The lion visits the lion.
True
2
proof
[(((triple11) -> rule4) OR ((((triple12) -> rule3)) -> rule4))]
("lion" "visits" "lion" "+")
((triple11) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion does not visit the lion.
False
2
inv-proof
[(((triple11) -> rule4) OR ((((triple12) -> rule3)) -> rule4))]
("lion" "visits" "lion" "-")
((triple11) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The bear is big.
True
3
proof
[(((((triple4) -> rule3)) -> rule5))]
("bear" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear does not visit the lion.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule4) OR ((((((triple4) -> rule3)) -> rule5)) -> rule1))]
("bear" "visits" "lion" "-")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "nice" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
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 likes the bear.
Unknown
random
[@0: The cow likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "bear" "+")
@0: The bear chases the cow.[(triple1)] The bear is nice.[(triple2)] The bear is young.[(triple3)] The bear visits the cow.[(triple4)] The cow chases the bear.[(triple5)] The cow chases the lion.[(triple6)] The cow likes the lion.[(triple7)] The cow visits the bear.[(triple8)] The cow visits the lion.[(triple9 OR ((triple8) -> rule4))] The lion is big.[(triple10 OR ((triple11) -> rule5) OR ((((triple12) -> rule3)) -> rule5))] The lion visits the bear.[(triple11 OR ((triple12) -> rule3))] The lion visits the cow.[(triple12)] @1: The bear visits the bear.[(((triple4) -> rule3))] The cow is big.[(((triple8) -> rule5))] The lion visits the lion.[(((triple11) -> rule4) OR ((((triple12) -> rule3)) -> rule4))] @2: The bear is big.[(((((triple4) -> rule3)) -> rule5))] The bear visits the lion.[(((((triple4) -> rule3)) -> rule4) OR ((((((triple4) -> rule3)) -> rule5)) -> rule1))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear is young.
("bear" "is" "young" "+")
triple3
The bear visits the cow.
("bear" "visits" "cow" "+")
triple4
The cow chases the bear.
("cow" "chases" "bear" "+")
triple5
The cow chases the lion.
("cow" "chases" "lion" "+")
triple6
The cow likes the lion.
("cow" "likes" "lion" "+")
triple7
The cow visits the bear.
("cow" "visits" "bear" "+")
triple8
The cow visits the lion.
("cow" "visits" "lion" "+")
triple9
((triple8) -> (rule4 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
triple10
((triple11) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
triple11
((triple12) -> (rule3 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
triple12
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple4) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((triple8) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple11) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The bear is big.
("bear" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear visits the lion.
("bear" "visits" "lion" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3