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