Charlie is blue. Charlie is furry. Charlie is kind. Charlie is quiet. Charlie is not red. Charlie is round. Charlie is not young. Gary is furry. Gary is quiet. Gary is not round. Harry is not blue. Harry is furry. Harry is not kind. Harry is quiet. Harry is not red. Harry is not round. If Harry is round then Harry is kind. If someone is red and not furry then they are blue. Round people are blue. All blue, red people are round. If Gary is furry then Gary is red. Quiet, red people are young. If someone is round and not red then they are kind. If Gary is kind and Gary is red then Gary is young.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not round.
("Gary" "is" "round" "-")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is not round.
("Harry" "is" "round" "-")
If Harry is round then Harry is kind.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "kind" "+"))
If someone is red and not furry then they are blue.
((("someone" "is" "red" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "blue" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All blue, red people are round.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If Gary is furry then Gary is red.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "red" "+"))
Quiet, red people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is round and not red then they are kind.
((("someone" "is" "round" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "kind" "+"))
If Gary is kind and Gary is red then Gary is young.
((("Gary" "is" "kind" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "young" "+"))
Gary is quiet.
True
1
proof
[(triple9)]
("Gary" "is" "quiet" "+")
triple9
Charlie is not kind.
False
1
inv-proof
[(triple3 OR ((triple6 triple5) -> rule7))]
("Charlie" "is" "kind" "-")
triple3
((triple6 triple5) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Gary is red.
True
2
proof
[(((triple8) -> rule5))]
("Gary" "is" "red" "+")
((triple8) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple8) -> rule5))]
("Gary" "is" "red" "-")
((triple8) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
True
4
proof
[(((triple9 ((triple8) -> rule5)) -> rule6))]
("Gary" "is" "young" "+")
((triple9 ((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not young.
False
4
inv-proof
[(((triple9 ((triple8) -> rule5)) -> rule6))]
("Gary" "is" "young" "-")
((triple9 ((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "young" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "kind" "+")
@0: Charlie is blue.[(triple1 OR ((triple6) -> rule3))] Charlie is furry.[(triple2)] Charlie is kind.[(triple3 OR ((triple6 triple5) -> rule7))] Charlie is not red.[(triple5)] Charlie is not young.[(triple7)] Charlie is quiet.[(triple4)] Charlie is round.[(triple6)] Gary is furry.[(triple8)] Gary is not round.[(triple10)] Gary is quiet.[(triple9)] Harry is furry.[(triple12)] Harry is not blue.[(triple11)] Harry is not kind.[(triple13)] Harry is not red.[(triple15)] Harry is not round.[(triple16)] Harry is quiet.[(triple14)] @1: Gary is red.[(((triple8) -> rule5))] @2: Gary is young.[(((triple9 ((triple8) -> rule5)) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple6) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple6 triple5) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
triple5
Charlie is not young.
("Charlie" "is" "young" "-")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is not round.
("Gary" "is" "round" "-")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is not blue.
("Harry" "is" "blue" "-")
triple11
Harry is not kind.
("Harry" "is" "kind" "-")
triple13
Harry is not red.
("Harry" "is" "red" "-")
triple15
Harry is not round.
("Harry" "is" "round" "-")
triple16
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Gary is red.
("Gary" "is" "red" "+")
((triple8) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple9 ((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2