Charlie is blue. Charlie is cold. Charlie is red. If Charlie is blue and Charlie is cold then Charlie is kind. If Charlie is kind then Charlie is big. If Charlie is big and Charlie is cold then Charlie is quiet. If Charlie is kind then Charlie is nice. All nice, quiet things are big. All cold, big things are nice.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
If Charlie is blue and Charlie is cold then Charlie is kind.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "kind" "+"))
If Charlie is kind then Charlie is big.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "big" "+"))
If Charlie is big and Charlie is cold then Charlie is quiet.
((("Charlie" "is" "big" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "quiet" "+"))
If Charlie is kind then Charlie is nice.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "nice" "+"))
All nice, quiet things are big.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
All cold, big things are nice.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is kind.
True
3
proof
[(((triple1 triple2) -> rule1))]
("Charlie" "is" "kind" "+")
((triple1 triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
3
inv-proof
[(((triple1 triple2) -> rule1))]
("Charlie" "is" "kind" "-")
((triple1 triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
True
4
proof
[(((((triple1 triple2) -> rule1)) -> rule2))]
("Charlie" "is" "big" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not big.
False
4
inv-proof
[(((((triple1 triple2) -> rule1)) -> rule2))]
("Charlie" "is" "big" "-")
((((triple1 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
True
6
proof
[(((((((triple1 triple2) -> rule1)) -> rule2) triple2) -> rule3))]
("Charlie" "is" "quiet" "+")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not quiet.
False
6
inv-proof
[(((((((triple1 triple2) -> rule1)) -> rule2) triple2) -> rule3))]
("Charlie" "is" "quiet" "-")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is red.[(triple3)] @1: Charlie is kind.[(((triple1 triple2) -> rule1))] @2: Charlie is big.[(((((triple1 triple2) -> rule1)) -> rule2))] Charlie is nice.[(((((triple1 triple2) -> rule1)) -> rule4) OR ((triple2 ((((triple1 triple2) -> rule1)) -> rule2)) -> rule6))] @3: Charlie is quiet.[(((((((triple1 triple2) -> rule1)) -> rule2) triple2) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1 triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((triple2 ((((triple1 triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3