Charlie is kind. Charlie is nice. Charlie is smart. Gary is blue. Gary is kind. Gary is nice. Gary is smart. Kind, green people are red. If someone is red then they are green. Nice people are green. If someone is kind and not blue then they are not smart. If Charlie is blue and Charlie is nice then Charlie is red. If someone is kind and not red then they are round.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Kind, green people are red.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is kind and not blue then they are not smart.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "smart" "-"))
If Charlie is blue and Charlie is nice then Charlie is red.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "red" "+"))
If someone is kind and not red then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "round" "+"))
Gary is smart.
True
1
proof
[(triple7)]
("Gary" "is" "smart" "+")
triple7
Gary is not blue.
False
1
inv-proof
[(triple4)]
("Gary" "is" "blue" "-")
triple4
Charlie is green.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "green" "+")
((triple2) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple6) -> rule3))]
("Gary" "is" "green" "-")
((triple6) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
True
4
proof
[(((triple5 ((triple6) -> rule3)) -> rule1))]
("Gary" "is" "red" "+")
((triple5 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not red.
False
4
inv-proof
[(((triple5 ((triple6) -> rule3)) -> rule1))]
("Gary" "is" "red" "-")
((triple5 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "round" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "round" "+")
@0: Charlie is kind.[(triple1)] Charlie is nice.[(triple2)] Charlie is smart.[(triple3)] Gary is blue.[(triple4)] Gary is kind.[(triple5)] Gary is nice.[(triple6)] Gary is smart.[(triple7)] @1: Charlie is green.[(((triple2) -> rule3))] Gary is green.[(((triple6) -> rule3))] @2: Charlie is red.[(((triple1 ((triple2) -> rule3)) -> rule1))] Gary is red.[(((triple5 ((triple6) -> rule3)) -> rule1))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple6) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple5 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2