Charlie is big. Charlie is blue. Charlie is cold. Charlie is red. Charlie is rough. Charlie is round. Charlie is white. Harry is big. Harry is blue. Harry is cold. Harry is red. Harry is rough. Harry is round. Harry is white. If Harry is red and Harry is not blue then Harry is not big. Cold people are rough. If someone is red and cold then they are white.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is red and Harry is not blue then Harry is not big.
((("Harry" "is" "red" "+") ("Harry" "is" "blue" "~")) -> ("Harry" "is" "big" "-"))
Cold people are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is red and cold then they are white.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Charlie is cold.
True
1
proof
[(triple3)]
("Charlie" "is" "cold" "+")
triple3
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is cold.[(triple3)] Charlie is red.[(triple4)] Charlie is rough.[(triple5 OR ((triple3) -> rule2))] Charlie is round.[(triple6)] Charlie is white.[(triple7 OR ((triple4 triple3) -> rule3))] Harry is big.[(triple8)] Harry is blue.[(triple9)] Harry is cold.[(triple10)] Harry is red.[(triple11)] Harry is rough.[(triple12 OR ((triple10) -> rule2))] Harry is round.[(triple13)] Harry is white.[(triple14 OR ((triple11 triple10) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple4 triple3) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
((triple10) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14
((triple11 triple10) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1