Charlie is blue. Charlie is cold. Charlie is not furry. Charlie is green. Charlie is kind. Charlie is nice. Charlie is not red. Fiona is blue. Fiona is cold. Fiona is not furry. Fiona is green. Fiona is kind. Fiona is nice. Fiona is red. Blue things are green. If something is blue and not green then it is cold. If something is blue then it is cold. If something is furry and cold then it is kind. All blue things are nice. If something is furry and not kind then it is nice.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is blue and not green then it is cold.
((("something" "is" "blue" "+") ("something" "is" "green" "~")) -> ("something" "is" "cold" "+"))
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is furry and cold then it is kind.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is furry and not kind then it is nice.
((("something" "is" "furry" "+") ("something" "is" "kind" "~")) -> ("something" "is" "nice" "+"))
Fiona is blue.
True
1
proof
[(triple8)]
("Fiona" "is" "blue" "+")
triple8
Charlie is red.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "red" "+")
triple7
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2 OR ((triple1) -> rule3))] Charlie is green.[(triple4 OR ((triple1) -> rule1))] Charlie is kind.[(triple5)] Charlie is nice.[(triple6 OR ((triple1) -> rule5))] Charlie is not furry.[(triple3)] Charlie is not red.[(triple7)] Fiona is blue.[(triple8)] Fiona is cold.[(triple9 OR ((triple8) -> rule3))] Fiona is green.[(triple11 OR ((triple8) -> rule1))] Fiona is kind.[(triple12)] Fiona is nice.[(triple13 OR ((triple8) -> rule5))] Fiona is not furry.[(triple10)] Fiona is red.[(triple14)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((triple1) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple3
Charlie is not red.
("Charlie" "is" "red" "-")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
((triple8) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple11
((triple8) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple12
Fiona is nice.
("Fiona" "is" "nice" "+")
triple13
((triple8) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple10
Fiona is red.
("Fiona" "is" "red" "+")
triple14