Charlie is not furry. Charlie is green. Charlie is quiet. White, quiet things are not nice. Quiet things are kind. If Charlie is cold and Charlie is nice then Charlie is green. White, cold things are green. All white, nice things are not green. Quiet things are not cold. Kind things are white. If something is furry and cold then it is quiet.
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
White, quiet things are not nice.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "-"))
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If Charlie is cold and Charlie is nice then Charlie is green.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "green" "+"))
White, cold things are green.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
All white, nice things are not green.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "-"))
Quiet things are not cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "-"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is furry and cold then it is quiet.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Charlie is not green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
Charlie is not cold.
True
2
proof
[(((triple3) -> rule6))]
("Charlie" "is" "cold" "-")
((triple3) -> (rule6 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
True
3
proof
[(((((triple3) -> rule2)) -> rule7))]
("Charlie" "is" "white" "+")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule7))]
("Charlie" "is" "white" "-")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not nice.
True
5
proof
[(((((((triple3) -> rule2)) -> rule7) triple3) -> rule1))]
("Charlie" "is" "nice" "-")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2)) triple3) -> (rule1 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
False
5
inv-proof
[(((((((triple3) -> rule2)) -> rule7) triple3) -> rule1))]
("Charlie" "is" "nice" "+")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2)) triple3) -> (rule1 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
@0: Charlie is green.[(triple2)] Charlie is not furry.[(triple1)] Charlie is quiet.[(triple3)] @1: Charlie is kind.[(((triple3) -> rule2))] Charlie is not cold.[(((triple3) -> rule6))] @2: Charlie is white.[(((((triple3) -> rule2)) -> rule7))] @3: Charlie is not nice.[(((((((triple3) -> rule2)) -> rule7) triple3) -> rule1))]
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
((triple3) -> (rule6 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not nice.
("Charlie" "is" "nice" "-")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2)) triple3) -> (rule1 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3