The bear does not need the cat. The bear visits the cat. The cat is kind. If something needs the cat then the cat needs the bear. If something visits the cat and the cat is nice then the cat needs the bear. If the bear does not visit the cat then the bear does not need the cat. If something is young and it likes the bear then the bear is not big. If something needs the bear then the bear does not like the cat. If something visits the bear and it does not visit the cat then it does not like the cat. If something is kind then it needs the cat. If something likes the cat then it needs the bear.
The bear does not need the cat.
("bear" "needs" "cat" "-")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat is kind.
("cat" "is" "kind" "+")
If something needs the cat then the cat needs the bear.
((("something" "needs" "cat" "+")) -> ("cat" "needs" "bear" "+"))
If something visits the cat and the cat is nice then the cat needs the bear.
((("something" "visits" "cat" "+") ("cat" "is" "nice" "+")) -> ("cat" "needs" "bear" "+"))
If the bear does not visit the cat then the bear does not need the cat.
((("bear" "visits" "cat" "~")) -> ("bear" "needs" "cat" "-"))
If something is young and it likes the bear then the bear is not big.
((("something" "is" "young" "+") ("something" "likes" "bear" "+")) -> ("bear" "is" "big" "-"))
If something needs the bear then the bear does not like the cat.
((("something" "needs" "bear" "+")) -> ("bear" "likes" "cat" "-"))
If something visits the bear and it does not visit the cat then it does not like the cat.
((("something" "visits" "bear" "+") ("something" "visits" "cat" "~")) -> ("something" "likes" "cat" "-"))
If something is kind then it needs the cat.
((("something" "is" "kind" "+")) -> ("something" "needs" "cat" "+"))
If something likes the cat then it needs the bear.
((("something" "likes" "cat" "+")) -> ("something" "needs" "bear" "+"))
The bear does not need the cat.
True
1
proof
[(triple1)]
("bear" "needs" "cat" "-")
triple1
The bear needs the cat.
False
1
inv-proof
[(triple1)]
("bear" "needs" "cat" "+")
triple1
The cat needs the cat.
True
2
proof
[(((triple3) -> rule7))]
("cat" "needs" "cat" "+")
((triple3) -> (rule7 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple3) -> rule7))]
("cat" "needs" "cat" "-")
((triple3) -> (rule7 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat needs the bear.
True
3
proof
[(((((triple3) -> rule7)) -> rule1))]
("cat" "needs" "bear" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat does not need the bear.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule1))]
("cat" "needs" "bear" "-")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The bear does not like the cat.
True
4
proof
[(((((((triple3) -> rule7)) -> rule1)) -> rule5))]
("bear" "likes" "cat" "-")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear does not like the cat.
("bear" "likes" "cat" "-")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The bear likes the cat.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule1)) -> rule5))]
("bear" "likes" "cat" "+")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear does not like the cat.
("bear" "likes" "cat" "-")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "needs" "bear" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The cat does not like the bear.
Unknown
inv-random
[@0: The cat likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "bear" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The bear does not need the cat.[(triple1)] The bear visits the cat.[(triple2)] The cat is kind.[(triple3)] @1: The cat needs the cat.[(((triple3) -> rule7))] @2: The cat needs the bear.[(((((triple3) -> rule7)) -> rule1))] @3: The bear does not like the cat.[(((((((triple3) -> rule7)) -> rule1)) -> rule5))]
The bear does not need the cat.
("bear" "needs" "cat" "-")
triple1
The bear visits the cat.
("bear" "visits" "cat" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple3) -> (rule7 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The bear does not like the cat.
("bear" "likes" "cat" "-")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear does not like the cat.
("bear" "likes" "cat" "-")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3