Charlie is blue. Charlie is kind. Charlie is nice. Charlie is red. Charlie is not young. Erin is blue. Erin is furry. Erin is not kind. Erin is nice. Erin is red. Erin is white. Erin is young. If someone is blue then they are furry. If Erin is not white then Erin is furry. If Erin is not white then Erin is kind. All furry people are nice. Furry people are nice. All kind people are nice. If someone is young then they are not kind. If Charlie is young and Charlie is nice then Charlie is not kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Erin is not white then Erin is furry.
((("Erin" "is" "white" "~")) -> ("Erin" "is" "furry" "+"))
If Erin is not white then Erin is kind.
((("Erin" "is" "white" "~")) -> ("Erin" "is" "kind" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is young then they are not kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "-"))
If Charlie is young and Charlie is nice then Charlie is not kind.
((("Charlie" "is" "young" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "kind" "-"))
Erin is not kind.
True
1
proof
[(triple8 OR ((triple12) -> rule7))]
("Erin" "is" "kind" "-")
triple8
((triple12) -> (rule7 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Charlie is not nice.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule6) OR ((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule1)) -> rule5))]
("Charlie" "is" "nice" "-")
triple3
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is furry.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
@0: Charlie is blue.[(triple1)] Charlie is kind.[(triple2)] Charlie is nice.[(triple3 OR ((triple2) -> rule6) OR ((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule1)) -> rule5))] Charlie is not young.[(triple5)] Charlie is red.[(triple4)] Erin is blue.[(triple6)] Erin is furry.[(triple7 OR ((triple6) -> rule1))] Erin is nice.[(triple9 OR ((triple7) -> rule4) OR ((triple7) -> rule5) OR ((((triple6) -> rule1)) -> rule4) OR ((((triple6) -> rule1)) -> rule5))] Erin is not kind.[(triple8 OR ((triple12) -> rule7))] Erin is red.[(triple10)] Erin is white.[(triple11)] Erin is young.[(triple12)] @1: Charlie is furry.[(((triple1) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not young.
("Charlie" "is" "young" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
((triple6) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple9
((triple7) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple7) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not kind.
("Erin" "is" "kind" "-")
triple8
((triple12) -> (rule7 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1