Anne is cold. Anne is kind. Anne is quiet. Anne is rough. Anne is smart. Anne is white. Anne is young. Charlie is cold. Charlie is kind. Charlie is quiet. Charlie is rough. Charlie is smart. Charlie is white. Charlie is young. If someone is kind and rough then they are cold. All smart, white people are kind.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If someone is kind and rough then they are cold.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
All smart, white people are kind.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Anne is white.
True
1
proof
[(triple6)]
("Anne" "is" "white" "+")
triple6
Charlie is not white.
False
1
inv-proof
[(triple13)]
("Charlie" "is" "white" "-")
triple13
@0: Anne is cold.[(triple1 OR ((triple2 triple4) -> rule1) OR ((((triple5 triple6) -> rule2) triple4) -> rule1))] Anne is kind.[(triple2 OR ((triple5 triple6) -> rule2))] Anne is quiet.[(triple3)] Anne is rough.[(triple4)] Anne is smart.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7)] Charlie is cold.[(triple8 OR ((triple9 triple11) -> rule1) OR ((((triple12 triple13) -> rule2) triple11) -> rule1))] Charlie is kind.[(triple9 OR ((triple12 triple13) -> rule2))] Charlie is quiet.[(triple10)] Charlie is rough.[(triple11)] Charlie is smart.[(triple12)] Charlie is white.[(triple13)] Charlie is young.[(triple14)]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple2 triple4) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple5 triple6) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple5 triple6) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
triple8
((triple9 triple11) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple12 triple13) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
((triple12 triple13) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
Charlie is smart.
("Charlie" "is" "smart" "+")
triple12
Charlie is white.
("Charlie" "is" "white" "+")
triple13
Charlie is young.
("Charlie" "is" "young" "+")
triple14