Anne is cold. Anne is green. Anne is kind. Anne is not nice. Anne is red. Anne is rough. Anne is not white. Charlie is cold. Charlie is not green. Charlie is not kind. Charlie is nice. Charlie is not red. Charlie is rough. Charlie is white. If Anne is red then Anne is kind. If Charlie is cold then Charlie is not kind.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not white.
("Anne" "is" "white" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If Anne is red then Anne is kind.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "kind" "+"))
If Charlie is cold then Charlie is not kind.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "kind" "-"))
Anne is red.
True
1
proof
[(triple5)]
("Anne" "is" "red" "+")
triple5
Anne is not kind.
False
1
inv-proof
[(triple3 OR ((triple5) -> rule1))]
("Anne" "is" "kind" "-")
triple3
((triple5) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is kind.[(triple3 OR ((triple5) -> rule1))] Anne is not nice.[(triple4)] Anne is not white.[(triple7)] Anne is red.[(triple5)] Anne is rough.[(triple6)] Charlie is cold.[(triple8)] Charlie is nice.[(triple11)] Charlie is not green.[(triple9)] Charlie is not kind.[(triple10 OR ((triple8) -> rule2))] Charlie is not red.[(triple12)] Charlie is rough.[(triple13)] Charlie is white.[(triple14)]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple5) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
triple4
Anne is not white.
("Anne" "is" "white" "-")
triple7
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple8
Charlie is nice.
("Charlie" "is" "nice" "+")
triple11
Charlie is not green.
("Charlie" "is" "green" "-")
triple9
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple10
((triple8) -> (rule2 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
triple13
Charlie is white.
("Charlie" "is" "white" "+")
triple14