The bear is big. The bear likes the cat. The bear likes the cow. The bear sees the cat. The bear sees the cow. The bear visits the cow. The cat is big. The cat is kind. The cat is young. The cat likes the bear. The cat likes the cow. The cat sees the bear. The cow is cold. The cow is young. The cow sees the bear. The cow visits the bear. If the cow is green and the cow is young then the cow is kind. If someone sees the bear and they are kind then the bear visits the cow. If someone visits the cow then the cow likes the bear. If someone likes the bear and they are cold then they are green. If someone likes the bear and the bear visits the cat then the cat is green. If someone is cold and green then they visit the cat.
The bear is big.
("bear" "is" "big" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is young.
("cow" "is" "young" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
If the cow is green and the cow is young then the cow is kind.
((("cow" "is" "green" "+") ("cow" "is" "young" "+")) -> ("cow" "is" "kind" "+"))
If someone sees the bear and they are kind then the bear visits the cow.
((("someone" "sees" "bear" "+") ("someone" "is" "kind" "+")) -> ("bear" "visits" "cow" "+"))
If someone visits the cow then the cow likes the bear.
((("someone" "visits" "cow" "+")) -> ("cow" "likes" "bear" "+"))
If someone likes the bear and they are cold then they are green.
((("someone" "likes" "bear" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone likes the bear and the bear visits the cat then the cat is green.
((("someone" "likes" "bear" "+") ("bear" "visits" "cat" "+")) -> ("cat" "is" "green" "+"))
If someone is cold and green then they visit the cat.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "visits" "cat" "+"))
The cow sees the bear.
True
1
proof
[(triple15)]
("cow" "sees" "bear" "+")
triple15
The cat does not like the cow.
False
1
inv-proof
[(triple11)]
("cat" "likes" "cow" "-")
triple11
The cow likes the bear.
True
2
proof
[(((triple6) -> rule3) OR ((((triple12 triple8) -> rule2)) -> rule3))]
("cow" "likes" "bear" "+")
((triple6) -> (rule3 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
((((triple12 triple8) -> (rule2 % int2))) -> (rule3 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The cow does not like the bear.
False
2
inv-proof
[(((triple6) -> rule3) OR ((((triple12 triple8) -> rule2)) -> rule3))]
("cow" "likes" "bear" "-")
((triple6) -> (rule3 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
((((triple12 triple8) -> (rule2 % int2))) -> (rule3 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The cow is green.
True
4
proof
[(((((triple6) -> rule3) triple13) -> rule4) OR ((((((triple12 triple8) -> rule2)) -> rule3) triple13) -> rule4))]
("cow" "is" "green" "+")
((((triple6) -> (rule3 % int2)) triple13) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
((((((triple12 triple8) -> (rule2 % int3))) -> (rule3 % int2)) triple13) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
The cow is not green.
False
4
inv-proof
[(((((triple6) -> rule3) triple13) -> rule4) OR ((((((triple12 triple8) -> rule2)) -> rule3) triple13) -> rule4))]
("cow" "is" "green" "-")
((((triple6) -> (rule3 % int2)) triple13) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
((((((triple12 triple8) -> (rule2 % int3))) -> (rule3 % int2)) triple13) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
The bear does not visit the cat.
Unknown
inv-rconc
[@1: The bear visits the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "visits" "cat" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat is not green.
Unknown
inv-rconc
[@2: The cat is green.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("cat" "is" "green" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bear is big.[(triple1)] The bear likes the cat.[(triple2)] The bear likes the cow.[(triple3)] The bear sees the cat.[(triple4)] The bear sees the cow.[(triple5)] The bear visits the cow.[(triple6 OR ((triple12 triple8) -> rule2))] The cat is big.[(triple7)] The cat is kind.[(triple8)] The cat is young.[(triple9)] The cat likes the bear.[(triple10)] The cat likes the cow.[(triple11)] The cat sees the bear.[(triple12)] The cow is cold.[(triple13)] The cow is young.[(triple14)] The cow sees the bear.[(triple15)] The cow visits the bear.[(triple16)] @1: The cow likes the bear.[(((triple6) -> rule3) OR ((((triple12 triple8) -> rule2)) -> rule3))] @2: The cow is green.[(((((triple6) -> rule3) triple13) -> rule4) OR ((((((triple12 triple8) -> rule2)) -> rule3) triple13) -> rule4))] @3: The cow is kind.[(((((((triple6) -> rule3) triple13) -> rule4) triple14) -> rule1) OR ((((((((triple12 triple8) -> rule2)) -> rule3) triple13) -> rule4) triple14) -> rule1))] The cow visits the cat.[(((triple13 ((((triple6) -> rule3) triple13) -> rule4)) -> rule6) OR ((triple13 ((((((triple12 triple8) -> rule2)) -> rule3) triple13) -> rule4)) -> rule6))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear likes the cat.
("bear" "likes" "cat" "+")
triple2
The bear likes the cow.
("bear" "likes" "cow" "+")
triple3
The bear sees the cat.
("bear" "sees" "cat" "+")
triple4
The bear sees the cow.
("bear" "sees" "cow" "+")
triple5
The bear visits the cow.
("bear" "visits" "cow" "+")
triple6
((triple12 triple8) -> (rule2 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The cat is big.
("cat" "is" "big" "+")
triple7
The cat is kind.
("cat" "is" "kind" "+")
triple8
The cat is young.
("cat" "is" "young" "+")
triple9
The cat likes the bear.
("cat" "likes" "bear" "+")
triple10
The cat likes the cow.
("cat" "likes" "cow" "+")
triple11
The cat sees the bear.
("cat" "sees" "bear" "+")
triple12
The cow is cold.
("cow" "is" "cold" "+")
triple13
The cow is young.
("cow" "is" "young" "+")
triple14
The cow sees the bear.
("cow" "sees" "bear" "+")
triple15
The cow visits the bear.
("cow" "visits" "bear" "+")
triple16
The cow likes the bear.
("cow" "likes" "bear" "+")
((triple6) -> (rule3 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
((((triple12 triple8) -> (rule2 % int2))) -> (rule3 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The cow is green.
("cow" "is" "green" "+")
((((triple6) -> (rule3 % int2)) triple13) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
((((((triple12 triple8) -> (rule2 % int3))) -> (rule3 % int2)) triple13) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
((((((triple6) -> (rule3 % int3)) triple13) -> (rule4 % int2)) triple14) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the bear.
("cow" "likes" "bear" "+")
int3
((((((((triple12 triple8) -> (rule2 % int4))) -> (rule3 % int3)) triple13) -> (rule4 % int2)) triple14) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the bear.
("cow" "likes" "bear" "+")
int3
The bear visits the cow.
("bear" "visits" "cow" "+")
int4
The cow visits the cat.
("cow" "visits" "cat" "+")
((triple13 ((((triple6) -> (rule3 % int3)) triple13) -> (rule4 % int2))) -> (rule6 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the bear.
("cow" "likes" "bear" "+")
int3
((triple13 ((((((triple12 triple8) -> (rule2 % int4))) -> (rule3 % int3)) triple13) -> (rule4 % int2))) -> (rule6 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the bear.
("cow" "likes" "bear" "+")
int3
The bear visits the cow.
("bear" "visits" "cow" "+")
int4