The bear is not kind. The bear is rough. The bear likes the cow. The bear does not need the cat. The cat is not blue. The cat is rough. The cat likes the bear. The cow is kind. The cow likes the cat. The cow does not need the bear. The cow visits the bear. The cow visits the cat. If someone likes the cow and they do not need the cat then the cat needs the bear. If the bear visits the cat then the bear is kind. If someone needs the bear and the bear is rough then they need the cow. If someone needs the cow then they visit the cow. If someone needs the bear and they are blue then they visit the cat. If the cow visits the bear then the bear likes the cat. If someone visits the bear and they are not nice then they like the cat. If the bear visits the cow and the bear is not nice then the cow likes the cat.
The bear is not kind.
("bear" "is" "kind" "-")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear does not need the cat.
("bear" "needs" "cat" "-")
The cat is not blue.
("cat" "is" "blue" "-")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow does not need the bear.
("cow" "needs" "bear" "-")
The cow visits the bear.
("cow" "visits" "bear" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If someone likes the cow and they do not need the cat then the cat needs the bear.
((("someone" "likes" "cow" "+") ("someone" "needs" "cat" "~")) -> ("cat" "needs" "bear" "+"))
If the bear visits the cat then the bear is kind.
((("bear" "visits" "cat" "+")) -> ("bear" "is" "kind" "+"))
If someone needs the bear and the bear is rough then they need the cow.
((("someone" "needs" "bear" "+") ("bear" "is" "rough" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the cow then they visit the cow.
((("someone" "needs" "cow" "+")) -> ("someone" "visits" "cow" "+"))
If someone needs the bear and they are blue then they visit the cat.
((("someone" "needs" "bear" "+") ("someone" "is" "blue" "+")) -> ("someone" "visits" "cat" "+"))
If the cow visits the bear then the bear likes the cat.
((("cow" "visits" "bear" "+")) -> ("bear" "likes" "cat" "+"))
If someone visits the bear and they are not nice then they like the cat.
((("someone" "visits" "bear" "+") ("someone" "is" "nice" "~")) -> ("someone" "likes" "cat" "+"))
If the bear visits the cow and the bear is not nice then the cow likes the cat.
((("bear" "visits" "cow" "+") ("bear" "is" "nice" "~")) -> ("cow" "likes" "cat" "+"))
The bear is not kind.
True
1
proof
[(triple1)]
("bear" "is" "kind" "-")
triple1
The cat is blue.
False
1
inv-proof
[(triple5)]
("cat" "is" "blue" "+")
triple5
The cat needs the bear.
True
3
proof
[(((triple3 triple4) -> rule1))]
("cat" "needs" "bear" "+")
((triple3 triple4) -> (rule1 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat does not need the bear.
False
3
inv-proof
[(((triple3 triple4) -> rule1))]
("cat" "needs" "bear" "-")
((triple3 triple4) -> (rule1 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat needs the cow.
True
5
proof
[(((((triple3 triple4) -> rule1) triple2) -> rule3))]
("cat" "needs" "cow" "+")
((((triple3 triple4) -> (rule1 % int2)) triple2) -> (rule3 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The cat does not need the cow.
False
5
inv-proof
[(((((triple3 triple4) -> rule1) triple2) -> rule3))]
("cat" "needs" "cow" "-")
((((triple3 triple4) -> (rule1 % int2)) triple2) -> (rule3 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The cat visits the cow.
True
6
proof
[(((((((triple3 triple4) -> rule1) triple2) -> rule3)) -> rule4))]
("cat" "visits" "cow" "+")
((((((triple3 triple4) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
int3
The cat does not visit the cow.
False
6
inv-proof
[(((((((triple3 triple4) -> rule1) triple2) -> rule3)) -> rule4))]
("cat" "visits" "cow" "-")
((((((triple3 triple4) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
int3
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "likes" "cat" "-")
The cow visits the cow.
Unknown
rconc
[@2: The cow visits the cow.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("cow" "visits" "cow" "+")
The bear does not visit the cow.
Unknown
inv-rconc
[@2: The bear visits the cow.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("bear" "visits" "cow" "-")
The bear visits the cat.
Unknown
rconc
[@1: The bear visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "visits" "cat" "+")
The cow does not like the bear.
Unknown
inv-random
[@0: The cow likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "bear" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The cow does not need the cat.
Unknown
inv-random
[@0: The cow needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cat" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear does not need the cat.[(triple4)] The bear is not kind.[(triple1)] The bear is rough.[(triple2)] The bear likes the cow.[(triple3)] The cat is not blue.[(triple5)] The cat is rough.[(triple6)] The cat likes the bear.[(triple7)] The cow does not need the bear.[(triple10)] The cow is kind.[(triple8)] The cow likes the cat.[(triple9)] The cow visits the bear.[(triple11)] The cow visits the cat.[(triple12)] @1: The bear likes the cat.[(((triple11) -> rule6))] The cat needs the bear.[(((triple3 triple4) -> rule1))] @2: The cat needs the cow.[(((((triple3 triple4) -> rule1) triple2) -> rule3))] @3: The cat visits the cow.[(((((((triple3 triple4) -> rule1) triple2) -> rule3)) -> rule4))]
The bear does not need the cat.
("bear" "needs" "cat" "-")
triple4
The bear is not kind.
("bear" "is" "kind" "-")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear likes the cow.
("bear" "likes" "cow" "+")
triple3
The cat is not blue.
("cat" "is" "blue" "-")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat likes the bear.
("cat" "likes" "bear" "+")
triple7
The cow does not need the bear.
("cow" "needs" "bear" "-")
triple10
The cow is kind.
("cow" "is" "kind" "+")
triple8
The cow likes the cat.
("cow" "likes" "cat" "+")
triple9
The cow visits the bear.
("cow" "visits" "bear" "+")
triple11
The cow visits the cat.
("cow" "visits" "cat" "+")
triple12
The bear likes the cat.
("bear" "likes" "cat" "+")
((triple11) -> (rule6 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
((triple3 triple4) -> (rule1 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
((((triple3 triple4) -> (rule1 % int2)) triple2) -> (rule3 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The cat visits the cow.
("cat" "visits" "cow" "+")
((((((triple3 triple4) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
int3