Anne is big. Anne is blue. Anne is not cold. Anne is kind. Anne is quiet. Anne is rough. Anne is white. Charlie is big. Charlie is blue. Charlie is cold. Charlie is kind. Charlie is quiet. Charlie is rough. Charlie is white. If Charlie is cold and Charlie is rough then Charlie is kind. Cold, kind things are rough. If Charlie is not quiet and Charlie is not cold then Charlie is rough. If Anne is not blue then Anne is rough. If something is blue then it is big. If something is quiet then it is big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
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 white.
("Charlie" "is" "white" "+")
If Charlie is cold and Charlie is rough then Charlie is kind.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "kind" "+"))
Cold, kind things are rough.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If Charlie is not quiet and Charlie is not cold then Charlie is rough.
((("Charlie" "is" "quiet" "~") ("Charlie" "is" "cold" "~")) -> ("Charlie" "is" "rough" "+"))
If Anne is not blue then Anne is rough.
((("Anne" "is" "blue" "~")) -> ("Anne" "is" "rough" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is quiet then it is big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Anne is quiet.
True
1
proof
[(triple5)]
("Anne" "is" "quiet" "+")
triple5
Anne is not kind.
False
1
inv-proof
[(triple4)]
("Anne" "is" "kind" "-")
triple4
@0: Anne is big.[(triple1 OR ((triple2) -> rule5) OR ((triple5) -> rule6))] Anne is blue.[(triple2)] Anne is kind.[(triple4)] Anne is not cold.[(triple3)] Anne is quiet.[(triple5)] Anne is rough.[(triple6)] Anne is white.[(triple7)] Charlie is big.[(triple8 OR ((triple12) -> rule6) OR ((triple9) -> rule5))] Charlie is blue.[(triple9)] Charlie is cold.[(triple10)] Charlie is kind.[(triple11 OR ((triple10 triple13) -> rule1))] Charlie is quiet.[(triple12)] Charlie is rough.[(triple13 OR ((triple10 triple11) -> rule2))] Charlie is white.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple5) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is not cold.
("Anne" "is" "cold" "-")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
triple8
((triple12) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple9) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple9
Charlie is cold.
("Charlie" "is" "cold" "+")
triple10
Charlie is kind.
("Charlie" "is" "kind" "+")
triple11
((triple10 triple13) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
triple13
((triple10 triple11) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple14