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