Charlie is blue. Charlie is cold. Charlie is green. Charlie is red. Charlie is rough. Charlie is white. Erin is blue. Erin is cold. Erin is not green. Erin is kind. Erin is not red. Erin is rough. All rough, blue things are kind. If something is blue and not green then it is kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is rough.
("Erin" "is" "rough" "+")
All rough, blue things are kind.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is blue and not green then it is kind.
((("something" "is" "blue" "+") ("something" "is" "green" "~")) -> ("something" "is" "kind" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Erin is not rough.
False
1
inv-proof
[(triple12)]
("Erin" "is" "rough" "-")
triple12
Charlie is kind.
True
3
proof
[(((triple5 triple1) -> rule1))]
("Charlie" "is" "kind" "+")
((triple5 triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
3
inv-proof
[(((triple5 triple1) -> rule1))]
("Charlie" "is" "kind" "-")
((triple5 triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is green.[(triple3)] Charlie is red.[(triple4)] Charlie is rough.[(triple5)] Charlie is white.[(triple6)] Erin is blue.[(triple7)] Erin is cold.[(triple8)] Erin is kind.[(triple10 OR ((triple12 triple7) -> rule1) OR ((triple7 triple9) -> rule2))] Erin is not green.[(triple9)] Erin is not red.[(triple11)] Erin is rough.[(triple12)] @1: Charlie is kind.[(((triple5 triple1) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is kind.
("Erin" "is" "kind" "+")
triple10
((triple12 triple7) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple7 triple9) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not green.
("Erin" "is" "green" "-")
triple9
Erin is not red.
("Erin" "is" "red" "-")
triple11
Erin is rough.
("Erin" "is" "rough" "+")
triple12
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple5 triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1