Charlie is kind. Charlie is round. Charlie is smart. If someone is nice and kind then they are green. All round people are kind. If Charlie is blue and Charlie is smart then Charlie is white. Blue, green people are round. All blue, nice people are white. All white people are green. If Charlie is green then Charlie is white. If someone is smart then they are nice.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If someone is nice and kind then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is blue and Charlie is smart then Charlie is white.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "white" "+"))
Blue, green people are round.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
All blue, nice people are white.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If Charlie is green then Charlie is white.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "white" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Charlie is smart.
True
1
proof
[(triple3)]
("Charlie" "is" "smart" "+")
triple3
Charlie is not kind.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule2))]
("Charlie" "is" "kind" "-")
triple1
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
True
2
proof
[(((triple3) -> rule8))]
("Charlie" "is" "nice" "+")
((triple3) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple3) -> rule8))]
("Charlie" "is" "nice" "-")
((triple3) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
True
4
proof
[(((((triple3) -> rule8) triple1) -> rule1) OR ((((triple3) -> rule8) ((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "green" "+")
((((triple3) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple3) -> (rule8 % int3)) ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not green.
False
4
inv-proof
[(((((triple3) -> rule8) triple1) -> rule1) OR ((((triple3) -> rule8) ((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "green" "-")
((((triple3) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple3) -> (rule8 % int3)) ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is white.
True
5
proof
[(((((((triple3) -> rule8) triple1) -> rule1)) -> rule7) OR ((((((triple3) -> rule8) ((triple2) -> rule2)) -> rule1)) -> rule7))]
("Charlie" "is" "white" "+")
((((((triple3) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple3) -> (rule8 % int4)) ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is not white.
False
5
inv-proof
[(((((((triple3) -> rule8) triple1) -> rule1)) -> rule7) OR ((((((triple3) -> rule8) ((triple2) -> rule2)) -> rule1)) -> rule7))]
("Charlie" "is" "white" "-")
((((((triple3) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple3) -> (rule8 % int4)) ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
@0: Charlie is kind.[(triple1 OR ((triple2) -> rule2))] Charlie is round.[(triple2)] Charlie is smart.[(triple3)] @1: Charlie is nice.[(((triple3) -> rule8))] @2: Charlie is green.[(((((triple3) -> rule8) triple1) -> rule1) OR ((((triple3) -> rule8) ((triple2) -> rule2)) -> rule1))] @3: Charlie is white.[(((((((triple3) -> rule8) triple1) -> rule1)) -> rule7) OR ((((((triple3) -> rule8) ((triple2) -> rule2)) -> rule1)) -> rule7))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple3) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple3) -> (rule8 % int3)) ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple3) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple3) -> (rule8 % int4)) ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4