Charlie is blue. Charlie is furry. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is smart. Erin is blue. Erin is green. Erin is kind. Erin is quiet. Erin is smart. All smart, green people are blue. If Erin is blue then Erin is red.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All smart, green people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Erin is blue then Erin is red.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "red" "+"))
Charlie is furry.
True
1
proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
Charlie is not blue.
False
1
inv-proof
[(triple1 OR ((triple7 triple3) -> rule1))]
("Charlie" "is" "blue" "-")
triple1
((triple7 triple3) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Erin is red.
True
2
proof
[(((triple8) -> rule2) OR ((((triple12 triple9) -> rule1)) -> rule2))]
("Erin" "is" "red" "+")
((triple8) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple12 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not red.
False
2
inv-proof
[(((triple8) -> rule2) OR ((((triple12 triple9) -> rule1)) -> rule2))]
("Erin" "is" "red" "-")
((triple8) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple12 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
@0: Charlie is blue.[(triple1 OR ((triple7 triple3) -> rule1))] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is kind.[(triple4)] Charlie is quiet.[(triple5)] Charlie is red.[(triple6)] Charlie is smart.[(triple7)] Erin is blue.[(triple8 OR ((triple12 triple9) -> rule1))] Erin is green.[(triple9)] Erin is kind.[(triple10)] Erin is quiet.[(triple11)] Erin is smart.[(triple12)] @1: Erin is red.[(((triple8) -> rule2) OR ((((triple12 triple9) -> rule1)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple7 triple3) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
((triple12 triple9) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Erin is red.
("Erin" "is" "red" "+")
((triple8) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple12 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2