Anne is white. Bob is kind. Gary is blue. Harry is green. Smart people are not kind. All young people are white. If someone is blue then they are young.
Anne is white.
("Anne" "is" "white" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Smart people are not kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "-"))
All young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is blue then they are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Gary is not blue.
False
1
inv-proof
[(triple3)]
("Gary" "is" "blue" "-")
triple3
Gary is young.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "young" "+")
((triple3) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "young" "-")
((triple3) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("Gary" "is" "white" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("Gary" "is" "white" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "young" "-")
Harry is white.
Unknown
rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "white" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "young" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is white.[(triple1)] Bob is kind.[(triple2)] Gary is blue.[(triple3)] Harry is green.[(triple4)] @1: Gary is young.[(((triple3) -> rule3))] @2: Gary is white.[(((((triple3) -> rule3)) -> rule2))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Gary is young.
("Gary" "is" "young" "+")
((triple3) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2