Charlie is not cold. Charlie is furry. Charlie is not green. Charlie is kind. Charlie is smart. Charlie is not white. Charlie is young. Dave is furry. Dave is kind. Dave is smart. Dave is white. Dave is not young. If someone is white then they are green. If someone is white and not furry then they are not green. All kind, young people are not green. All young, furry people are not white. Smart, white people are kind. All green, kind people are cold.
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is not young.
("Dave" "is" "young" "-")
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is white and not furry then they are not green.
((("someone" "is" "white" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "green" "-"))
All kind, young people are not green.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "-"))
All young, furry people are not white.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "-"))
Smart, white people are kind.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All green, kind people are cold.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Charlie is kind.
True
1
proof
[(triple4)]
("Charlie" "is" "kind" "+")
triple4
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Dave is green.
True
2
proof
[(((triple11) -> rule1))]
("Dave" "is" "green" "+")
((triple11) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple11) -> rule1))]
("Dave" "is" "green" "-")
((triple11) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
@0: Charlie is furry.[(triple2)] Charlie is kind.[(triple4)] Charlie is not cold.[(triple1)] Charlie is not green.[(triple3 OR ((triple4 triple7) -> rule3))] Charlie is not white.[(triple6 OR ((triple7 triple2) -> rule4))] Charlie is smart.[(triple5)] Charlie is young.[(triple7)] Dave is furry.[(triple8)] Dave is kind.[(triple9 OR ((triple10 triple11) -> rule5))] Dave is not young.[(triple12)] Dave is smart.[(triple10)] Dave is white.[(triple11)] @1: Dave is green.[(((triple11) -> rule1))] @2: Dave is cold.[(((((triple11) -> rule1) triple9) -> rule6) OR ((((triple11) -> rule1) ((triple10 triple11) -> rule5)) -> rule6))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple1
Charlie is not green.
("Charlie" "is" "green" "-")
triple3
((triple4 triple7) -> (rule3 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is not white.
("Charlie" "is" "white" "-")
triple6
((triple7 triple2) -> (rule4 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple9
((triple10 triple11) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
triple12
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Dave is green.
("Dave" "is" "green" "+")
((triple11) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple11) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple11) -> (rule1 % int3)) ((triple10 triple11) -> (rule5 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3