Charlie is kind. Charlie is nice. Charlie is rough. Charlie is round. Charlie is smart. Harry is blue. Harry is kind. Harry is nice. Harry is rough. Harry is round. Harry is smart. Harry is white. If Charlie is smart then Charlie is blue. All blue people are white.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If Charlie is smart then Charlie is blue.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "blue" "+"))
All blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Harry is kind.
True
1
proof
[(triple7)]
("Harry" "is" "kind" "+")
triple7
Charlie is not smart.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "smart" "-")
triple5
Charlie is blue.
True
2
proof
[(((triple5) -> rule1))]
("Charlie" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple5) -> rule1))]
("Charlie" "is" "blue" "-")
((triple5) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("Charlie" "is" "white" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule2))]
("Charlie" "is" "white" "-")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
@0: Charlie is kind.[(triple1)] Charlie is nice.[(triple2)] Charlie is rough.[(triple3)] Charlie is round.[(triple4)] Charlie is smart.[(triple5)] Harry is blue.[(triple6)] Harry is kind.[(triple7)] Harry is nice.[(triple8)] Harry is rough.[(triple9)] Harry is round.[(triple10)] Harry is smart.[(triple11)] Harry is white.[(triple12 OR ((triple6) -> rule2))] @1: Charlie is blue.[(((triple5) -> rule1))] @2: Charlie is white.[(((((triple5) -> rule1)) -> rule2))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple6) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2