Charlie is blue. Charlie is cold. Charlie is furry. Charlie is not green. Charlie is quiet. Charlie is round. Charlie is smart. Gary is cold. Gary is green. Gary is quiet. Cold, green people are not blue. If someone is round and quiet then they are furry. If Charlie is quiet and Charlie is furry then Charlie is smart.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Cold, green people are not blue.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "-"))
If someone is round and quiet then they are furry.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is quiet and Charlie is furry then Charlie is smart.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "smart" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Charlie is green.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "green" "+")
triple4
Gary is not blue.
True
3
proof
[(((triple8 triple9) -> rule1))]
("Gary" "is" "blue" "-")
((triple8 triple9) -> (rule1 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is blue.
False
3
inv-proof
[(((triple8 triple9) -> rule1))]
("Gary" "is" "blue" "+")
((triple8 triple9) -> (rule1 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is furry.[(triple3 OR ((triple6 triple5) -> rule2))] Charlie is not green.[(triple4)] Charlie is quiet.[(triple5)] Charlie is round.[(triple6)] Charlie is smart.[(triple7 OR ((triple5 triple3) -> rule3) OR ((triple5 ((triple6 triple5) -> rule2)) -> rule3))] Gary is cold.[(triple8)] Gary is green.[(triple9)] Gary is quiet.[(triple10)] @1: Gary is not blue.[(((triple8 triple9) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple6 triple5) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not green.
("Charlie" "is" "green" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
((triple5 triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple5 ((triple6 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is not blue.
("Gary" "is" "blue" "-")
((triple8 triple9) -> (rule1 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1