Charlie is green. Charlie is kind. Charlie is young. Red things are nice. Green things are nice. Green, blue things are young. Nice things are red. All red things are not smart. Nice, smart things are blue.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Green, blue things are young.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All red things are not smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "-"))
Nice, smart things are blue.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Charlie is kind.
True
1
proof
[(triple2)]
("Charlie" "is" "kind" "+")
triple2
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Charlie is nice.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not smart.
True
4
proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
("Charlie" "is" "smart" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is smart.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
("Charlie" "is" "smart" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
@0: Charlie is green.[(triple1)] Charlie is kind.[(triple2)] Charlie is young.[(triple3)] @1: Charlie is nice.[(((triple1) -> rule2))] @2: Charlie is red.[(((((triple1) -> rule2)) -> rule4))] @3: Charlie is not smart.[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not smart.
("Charlie" "is" "smart" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3