Charlie is nice. Charlie is not red. Charlie is rough. If something is nice then it is quiet. If Charlie is young then Charlie is blue. If something is nice and not red then it is young. If something is blue and not young then it is furry. All blue things are not furry. If something is nice and not quiet then it is blue. Red things are not blue. If something is red and not furry then it is rough.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is young then Charlie is blue.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "blue" "+"))
If something is nice and not red then it is young.
((("something" "is" "nice" "+") ("something" "is" "red" "~")) -> ("something" "is" "young" "+"))
If something is blue and not young then it is furry.
((("something" "is" "blue" "+") ("something" "is" "young" "~")) -> ("something" "is" "furry" "+"))
All blue things are not furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "-"))
If something is nice and not quiet then it is blue.
((("something" "is" "nice" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "blue" "+"))
Red things are not blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "-"))
If something is red and not furry then it is rough.
((("something" "is" "red" "+") ("something" "is" "furry" "~")) -> ("something" "is" "rough" "+"))
Charlie is rough.
True
1
proof
[(triple3)]
("Charlie" "is" "rough" "+")
triple3
Charlie is not nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "-")
triple1
Charlie is quiet.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
True
4
proof
[(((((triple1 triple2) -> rule3)) -> rule2))]
("Charlie" "is" "blue" "+")
((((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not blue.
False
4
inv-proof
[(((((triple1 triple2) -> rule3)) -> rule2))]
("Charlie" "is" "blue" "-")
((((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not furry.
True
5
proof
[(((((((triple1 triple2) -> rule3)) -> rule2)) -> rule5))]
("Charlie" "is" "furry" "-")
((((((triple1 triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is furry.
False
5
inv-proof
[(((((((triple1 triple2) -> rule3)) -> rule2)) -> rule5))]
("Charlie" "is" "furry" "+")
((((((triple1 triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
@0: Charlie is nice.[(triple1)] Charlie is not red.[(triple2)] Charlie is rough.[(triple3)] @1: Charlie is quiet.[(((triple1) -> rule1))] Charlie is young.[(((triple1 triple2) -> rule3))] @2: Charlie is blue.[(((((triple1 triple2) -> rule3)) -> rule2))] @3: Charlie is not furry.[(((((((triple1 triple2) -> rule3)) -> rule2)) -> rule5))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is not red.
("Charlie" "is" "red" "-")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not furry.
("Charlie" "is" "furry" "-")
((((((triple1 triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3