Charlie is big. Charlie is blue. Charlie is cold. Charlie is not green. Charlie is nice. Charlie is quiet. Charlie is smart. Fiona is not big. Fiona is blue. Fiona is cold. Fiona is green. Fiona is nice. Fiona is not quiet. Fiona is smart. If Charlie is nice then Charlie is big. All quiet people are cold. If someone is cold and not blue then they are not nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
If Charlie is nice then Charlie is big.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "big" "+"))
All quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and not blue then they are not nice.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "nice" "-"))
Charlie is smart.
True
1
proof
[(triple7)]
("Charlie" "is" "smart" "+")
triple7
Charlie is not nice.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "nice" "-")
triple5
@0: Charlie is big.[(triple1 OR ((triple5) -> rule1))] Charlie is blue.[(triple2)] Charlie is cold.[(triple3 OR ((triple6) -> rule2))] Charlie is nice.[(triple5)] Charlie is not green.[(triple4)] Charlie is quiet.[(triple6)] Charlie is smart.[(triple7)] Fiona is blue.[(triple9)] Fiona is cold.[(triple10)] Fiona is green.[(triple11)] Fiona is nice.[(triple12)] Fiona is not big.[(triple8)] Fiona is not quiet.[(triple13)] Fiona is smart.[(triple14)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple5) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
((triple6) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is not green.
("Charlie" "is" "green" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
Fiona is green.
("Fiona" "is" "green" "+")
triple11
Fiona is nice.
("Fiona" "is" "nice" "+")
triple12
Fiona is not big.
("Fiona" "is" "big" "-")
triple8
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple13
Fiona is smart.
("Fiona" "is" "smart" "+")
triple14