Charlie is cold. If Charlie is white then Charlie is red. If something is red then it is white. Cold, red things are rough. If something is green then it is cold. Rough, white things are red. Cold things are quiet.
Charlie is cold.
("Charlie" "is" "cold" "+")
If Charlie is white then Charlie is red.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "red" "+"))
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Cold, red things are rough.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Rough, white things are red.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Charlie is quiet.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is rough.
Unknown
rconc
[@4: Charlie is rough.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is cold.[(triple1)] @1: Charlie is quiet.[(((triple1) -> rule6))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1