Charlie is nice. Charlie is white. Charlie is young. Young people are quiet. All nice people are smart. If someone is smart and quiet then they are blue. All green people are nice. All blue, young people are nice. If Charlie is quiet then Charlie is blue.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
All nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and quiet then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
All blue, young people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is quiet then Charlie is blue.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "blue" "+"))
Charlie is young.
True
1
proof
[(triple3)]
("Charlie" "is" "young" "+")
triple3
Charlie is not young.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "young" "-")
triple3
Charlie is quiet.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple3) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
True
3
proof
[(((((triple3) -> rule1)) -> rule6) OR ((((triple1) -> rule2) ((triple3) -> rule1)) -> rule3))]
("Charlie" "is" "blue" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not blue.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6) OR ((((triple1) -> rule2) ((triple3) -> rule1)) -> rule3))]
("Charlie" "is" "blue" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
@0: Charlie is nice.[(triple1 OR ((((((triple3) -> rule1)) -> rule6) triple3) -> rule5))] Charlie is white.[(triple2)] Charlie is young.[(triple3)] @1: Charlie is quiet.[(((triple3) -> rule1))] Charlie is smart.[(((triple1) -> rule2) OR ((((((((triple3) -> rule1)) -> rule6) triple3) -> rule5)) -> rule2))] @2: Charlie is blue.[(((((triple3) -> rule1)) -> rule6) OR ((((triple1) -> rule2) ((triple3) -> rule1)) -> rule3))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2)) triple3) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((((((triple3) -> (rule1 % int4))) -> (rule6 % int3)) triple3) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3