Charlie is kind. All kind people are rough. Red, nice people are rough. If someone is red then they are nice. If someone is cold and nice then they are red. If someone is nice then they are red. Rough people are cold. Rough, blue people are kind. All kind, cold people are blue.
Charlie is kind.
("Charlie" "is" "kind" "+")
All kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Red, nice people are rough.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold and nice then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Rough, blue people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All kind, cold people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Charlie is kind.
True
1
proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Charlie is rough.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("Charlie" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not red.
Unknown
inv-rconc
[@3: Charlie is red.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is nice.
Unknown
rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is kind.[(triple1)] @1: Charlie is rough.[(((triple1) -> rule1))] @2: Charlie is cold.[(((((triple1) -> rule1)) -> rule6))] @3: Charlie is blue.[(((triple1 ((((triple1) -> rule1)) -> rule6)) -> rule8))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3