Anne is blue. Anne is green. Anne is kind. Anne is nice. Anne is red. Anne is not round. Anne is not young. Charlie is green. Charlie is nice. Charlie is red. Charlie is not round. Charlie is young. Kind people are blue. If someone is young and round then they are blue. All kind, blue people are red. If someone is young then they are kind. Young people are green. If someone is blue and not kind then they are not nice. All blue people are nice. If someone is round and not red then they are not nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is not round.
("Anne" "is" "round" "-")
Anne is not young.
("Anne" "is" "young" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is young and round then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All kind, blue people are red.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is young then they are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is blue and not kind then they are not nice.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "nice" "-"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is round and not red then they are not nice.
((("someone" "is" "round" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "nice" "-"))
Charlie is not round.
True
1
proof
[(triple11)]
("Charlie" "is" "round" "-")
triple11
Anne is young.
False
1
inv-proof
[(triple7)]
("Anne" "is" "young" "+")
triple7
Charlie is kind.
True
2
proof
[(((triple12) -> rule4))]
("Charlie" "is" "kind" "+")
((triple12) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple12) -> rule4))]
("Charlie" "is" "kind" "-")
((triple12) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
True
3
proof
[(((((triple12) -> rule4)) -> rule1))]
("Charlie" "is" "blue" "+")
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not blue.
False
3
inv-proof
[(((((triple12) -> rule4)) -> rule1))]
("Charlie" "is" "blue" "-")
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
@0: Anne is blue.[(triple1 OR ((triple3) -> rule1))] Anne is green.[(triple2)] Anne is kind.[(triple3)] Anne is nice.[(triple4 OR ((triple1) -> rule7) OR ((((triple3) -> rule1)) -> rule7))] Anne is not round.[(triple6)] Anne is not young.[(triple7)] Anne is red.[(triple5 OR ((triple3 triple1) -> rule3) OR ((triple3 ((triple3) -> rule1)) -> rule3))] Charlie is green.[(triple8 OR ((triple12) -> rule5))] Charlie is nice.[(triple9 OR ((((((triple12) -> rule4)) -> rule1)) -> rule7))] Charlie is not round.[(triple11)] Charlie is red.[(triple10 OR ((((triple12) -> rule4) ((((triple12) -> rule4)) -> rule1)) -> rule3))] Charlie is young.[(triple12)] @1: Charlie is kind.[(((triple12) -> rule4))] @2: Charlie is blue.[(((((triple12) -> rule4)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple3) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not round.
("Anne" "is" "round" "-")
triple6
Anne is not young.
("Anne" "is" "young" "-")
triple7
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple3 triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple8
((triple12) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
((((((triple12) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not round.
("Charlie" "is" "round" "-")
triple11
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((((triple12) -> (rule4 % int3)) ((((triple12) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple12
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple12) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2