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