Charlie is big. Charlie is blue. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is rough. Harry is big. Harry is blue. Harry is green. Harry is kind. Harry is nice. Harry is quiet. If someone is nice then they are quiet. If someone is kind and not nice then they are not quiet. If someone is quiet and not nice then they are not blue. Nice people are big. Nice people are rough. If Harry is not big then Harry is blue.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is nice then they are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind and not nice then they are not quiet.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "quiet" "-"))
If someone is quiet and not nice then they are not blue.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "blue" "-"))
Nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If Harry is not big then Harry is blue.
((("Harry" "is" "big" "~")) -> ("Harry" "is" "blue" "+"))
Charlie is quiet.
True
1
proof
[(triple5)]
("Charlie" "is" "quiet" "+")
triple5
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is green.[(triple3)] Charlie is kind.[(triple4)] Charlie is quiet.[(triple5)] Charlie is rough.[(triple6)] Harry is big.[(triple7 OR ((triple11) -> rule4))] Harry is blue.[(triple8)] Harry is green.[(triple9)] Harry is kind.[(triple10)] Harry is nice.[(triple11)] Harry is quiet.[(triple12 OR ((triple11) -> rule1))] @1: Harry is rough.[(((triple11) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple11) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
((triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple11) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1