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