Anne is white. Charlie is round. Gary is not big. Harry is round. If someone is green and nice then they are white. If Charlie is white then Charlie is round. All nice people are kind. If someone is white then they are kind. All nice people are not big. Kind, white people are round.
Anne is white.
("Anne" "is" "white" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is not big.
("Gary" "is" "big" "-")
Harry is round.
("Harry" "is" "round" "+")
If someone is green and nice then they are white.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If Charlie is white then Charlie is round.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "round" "+"))
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is white then they are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All nice people are not big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "-"))
Kind, white people are round.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Harry is round.
True
1
proof
[(triple4)]
("Harry" "is" "round" "+")
triple4
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Anne is kind.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "kind" "-")
((triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule6))]
("Anne" "is" "round" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not round.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule6))]
("Anne" "is" "round" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Gary" "is" "kind" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "+")
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Anne is white.[(triple1)] Charlie is round.[(triple2)] Gary is not big.[(triple3)] Harry is round.[(triple4)] @1: Anne is kind.[(((triple1) -> rule4))] @2: Anne is round.[(((((triple1) -> rule4) triple1) -> rule6))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Gary is not big.
("Gary" "is" "big" "-")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2