The bear is rough. If the bear is nice then the bear is young. If the bear is nice then the bear is not young. Nice people are rough. Rough people are cold. If the bear is young and the bear is blue then the bear is nice. All cold, rough people are not blue.
The bear is rough.
("bear" "is" "rough" "+")
If the bear is nice then the bear is young.
((("bear" "is" "nice" "+")) -> ("bear" "is" "young" "+"))
If the bear is nice then the bear is not young.
((("bear" "is" "nice" "+")) -> ("bear" "is" "young" "-"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If the bear is young and the bear is blue then the bear is nice.
((("bear" "is" "young" "+") ("bear" "is" "blue" "+")) -> ("bear" "is" "nice" "+"))
All cold, rough people are not blue.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "-"))
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 cold.
True
2
proof
[(((triple1) -> rule4))]
("bear" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "is" "cold" "-")
((triple1) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is not blue.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule6))]
("bear" "is" "blue" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
The bear is not blue.
("bear" "is" "blue" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is blue.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule6))]
("bear" "is" "blue" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
The bear is not blue.
("bear" "is" "blue" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "nice" "-")
The bear is young.
Unknown
rconc
[@2: The bear is young.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("bear" "is" "young" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
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 is rough.[(triple1)] @1: The bear is cold.[(((triple1) -> rule4))] @2: The bear is not blue.[(((((triple1) -> rule4) triple1) -> rule6))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is not blue.
("bear" "is" "blue" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
The bear is not blue.
("bear" "is" "blue" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2