The bear is rough. If the bear is rough and the bear is young then the bear is blue. Blue things are not green. Rough things are young. If something is young and not blue then it is nice. If the bear is blue then the bear is not green. If the bear is nice then the bear is green.
The bear is rough.
("bear" "is" "rough" "+")
If the bear is rough and the bear is young then the bear is blue.
((("bear" "is" "rough" "+") ("bear" "is" "young" "+")) -> ("bear" "is" "blue" "+"))
Blue things are not green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is young and not blue then it is nice.
((("something" "is" "young" "+") ("something" "is" "blue" "~")) -> ("something" "is" "nice" "+"))
If the bear is blue then the bear is not green.
((("bear" "is" "blue" "+")) -> ("bear" "is" "green" "-"))
If the bear is nice then the bear is green.
((("bear" "is" "nice" "+")) -> ("bear" "is" "green" "+"))
The bear is rough.
True
1
proof
[(triple1)]
("bear" "is" "rough" "+")
triple1
The bear is not rough.
False
1
inv-proof
[(triple1)]
("bear" "is" "rough" "-")
triple1
The bear is young.
True
2
proof
[(((triple1) -> rule3))]
("bear" "is" "young" "+")
((triple1) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "is" "young" "-")
((triple1) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is blue.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("bear" "is" "blue" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("bear" "is" "blue" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is not green.
True
5
proof
[(((((triple1 ((triple1) -> rule3)) -> rule1)) -> rule2) OR ((((triple1 ((triple1) -> rule3)) -> rule1)) -> rule5))]
("bear" "is" "green" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is green.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule1)) -> rule2) OR ((((triple1 ((triple1) -> rule3)) -> rule1)) -> rule5))]
("bear" "is" "green" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "nice" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear is rough.[(triple1)] @1: The bear is young.[(((triple1) -> rule3))] @2: The bear is blue.[(((triple1 ((triple1) -> rule3)) -> rule1))] @3: The bear is not green.[(((((triple1 ((triple1) -> rule3)) -> rule1)) -> rule2) OR ((((triple1 ((triple1) -> rule3)) -> rule1)) -> rule5))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is not green.
("bear" "is" "green" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3