Charlie is not blue. Charlie is nice. Charlie is quiet. Charlie is not rough. Charlie is smart. Charlie is white. Fiona is quiet. Fiona is not rough. Fiona is not smart. Fiona is white. Harry is blue. Harry is nice. Harry is quiet. Harry is not rough. Harry is smart. Harry is white. If someone is rough then they are not white. All quiet people are young. White people are nice. If someone is rough then they are not blue. If someone is smart and not white then they are blue. If Fiona is blue then Fiona is not smart.
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is rough then they are not white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "-"))
All quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
White people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough then they are not blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "-"))
If someone is smart and not white then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "blue" "+"))
If Fiona is blue then Fiona is not smart.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "smart" "-"))
Harry is smart.
True
1
proof
[(triple15)]
("Harry" "is" "smart" "+")
triple15
Harry is not nice.
False
1
inv-proof
[(triple12 OR ((triple16) -> rule3))]
("Harry" "is" "nice" "-")
triple12
((triple16) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Fiona is nice.
True
2
proof
[(((triple10) -> rule3))]
("Fiona" "is" "nice" "+")
((triple10) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "young" "-")
((triple3) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
@0: Charlie is nice.[(triple2 OR ((triple6) -> rule3))] Charlie is not blue.[(triple1)] Charlie is not rough.[(triple4)] Charlie is quiet.[(triple3)] Charlie is smart.[(triple5)] Charlie is white.[(triple6)] Fiona is not rough.[(triple8)] Fiona is not smart.[(triple9)] Fiona is quiet.[(triple7)] Fiona is white.[(triple10)] Harry is blue.[(triple11)] Harry is nice.[(triple12 OR ((triple16) -> rule3))] Harry is not rough.[(triple14)] Harry is quiet.[(triple13)] Harry is smart.[(triple15)] Harry is white.[(triple16)] @1: Charlie is young.[(((triple3) -> rule2))] Fiona is nice.[(((triple10) -> rule3))] Fiona is young.[(((triple7) -> rule2))] Harry is young.[(((triple13) -> rule2))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
((triple6) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple1
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple8
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple9
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
((triple16) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Charlie is young.
("Charlie" "is" "young" "+")
((triple3) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple10) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple13) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1