The bear is green. The bear visits the cat. The cat visits the bear. If someone sees the bear then the bear does not see the cat. If someone is green then they see the bear. If someone sees the bear and the bear does not see the cat then they are not young.
The bear is green.
("bear" "is" "green" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If someone sees the bear then the bear does not see the cat.
((("someone" "sees" "bear" "+")) -> ("bear" "sees" "cat" "-"))
If someone is green then they see the bear.
((("someone" "is" "green" "+")) -> ("someone" "sees" "bear" "+"))
If someone sees the bear and the bear does not see the cat then they are not young.
((("someone" "sees" "bear" "+") ("bear" "sees" "cat" "~")) -> ("someone" "is" "young" "-"))
The bear is green.
True
1
proof
[(triple1)]
("bear" "is" "green" "+")
triple1
The bear is not green.
False
1
inv-proof
[(triple1)]
("bear" "is" "green" "-")
triple1
The bear sees the bear.
True
2
proof
[(((triple1) -> rule2))]
("bear" "sees" "bear" "+")
((triple1) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear does not see the bear.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "sees" "bear" "-")
((triple1) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear does not see the cat.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("bear" "sees" "cat" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The bear does not see the cat.
("bear" "sees" "cat" "-")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear sees the cat.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("bear" "sees" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The bear does not see the cat.
("bear" "sees" "cat" "-")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is not young.
True
6
proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule1)) -> rule3))]
("bear" "is" "young" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The bear is not young.
("bear" "is" "young" "-")
int1
The bear does not see the cat.
("bear" "sees" "cat" "-")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The bear is young.
False
6
inv-proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule1)) -> rule3))]
("bear" "is" "young" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The bear is not young.
("bear" "is" "young" "-")
int1
The bear does not see the cat.
("bear" "sees" "cat" "-")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The cat does not see the bear.
Unknown
inv-rconc
[@1: The cat sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "bear" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
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 visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
@0: The bear is green.[(triple1)] The bear visits the cat.[(triple2)] The cat visits the bear.[(triple3)] @1: The bear sees the bear.[(((triple1) -> rule2))] @2: The bear does not see the cat.[(((((triple1) -> rule2)) -> rule1))] @3: The bear is not young.[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule1)) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear visits the cat.
("bear" "visits" "cat" "+")
triple2
The cat visits the bear.
("cat" "visits" "bear" "+")
triple3
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple1) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear does not see the cat.
("bear" "sees" "cat" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The bear does not see the cat.
("bear" "sees" "cat" "-")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is not young.
("bear" "is" "young" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The bear is not young.
("bear" "is" "young" "-")
int1
The bear does not see the cat.
("bear" "sees" "cat" "-")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3