Charlie is big. Charlie is green. Charlie is quiet. If someone is blue then they are big. All green people are not blue. All nice people are green. If Charlie is blue and Charlie is quiet then Charlie is nice. If Charlie is green then Charlie is nice. If Charlie is green then Charlie is not blue. If someone is nice and quiet then they are kind. If Charlie is not green then Charlie is young.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
If someone is blue then they are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All green people are not blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "-"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Charlie is blue and Charlie is quiet then Charlie is nice.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "nice" "+"))
If Charlie is green then Charlie is nice.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "nice" "+"))
If Charlie is green then Charlie is not blue.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "blue" "-"))
If someone is nice and quiet then they are kind.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is not green then Charlie is young.
((("Charlie" "is" "green" "~")) -> ("Charlie" "is" "young" "+"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Charlie is not quiet.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "quiet" "-")
triple3
Charlie is not blue.
True
2
proof
[(((triple2) -> rule2) OR ((triple2) -> rule6))]
("Charlie" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
((triple2) -> (rule6 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
True
4
proof
[(((((triple2) -> rule5) triple3) -> rule7))]
("Charlie" "is" "kind" "+")
((((triple2) -> (rule5 % int2)) triple3) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not kind.
False
4
inv-proof
[(((((triple2) -> rule5) triple3) -> rule7))]
("Charlie" "is" "kind" "-")
((((triple2) -> (rule5 % int2)) triple3) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
@0: Charlie is big.[(triple1)] Charlie is green.[(triple2)] Charlie is quiet.[(triple3)] @1: Charlie is nice.[(((triple2) -> rule5))] Charlie is not blue.[(((triple2) -> rule2) OR ((triple2) -> rule6))] @2: Charlie is kind.[(((((triple2) -> rule5) triple3) -> rule7))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not blue.
("Charlie" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
((triple2) -> (rule6 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule5 % int2)) triple3) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2