Anne is big. Anne is not cold. Anne is kind. Anne is nice. Anne is quiet. Anne is rough. Anne is white. Fiona is big. Fiona is cold. Fiona is kind. Fiona is nice. Fiona is not quiet. Fiona is not rough. Fiona is not white. If something is white and not cold then it is nice. If Fiona is cold then Fiona is kind. White things are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Fiona is not white.
("Fiona" "is" "white" "-")
If something is white and not cold then it is nice.
((("something" "is" "white" "+") ("something" "is" "cold" "~")) -> ("something" "is" "nice" "+"))
If Fiona is cold then Fiona is kind.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "kind" "+"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Anne is big.
True
1
proof
[(triple1 OR ((triple7) -> rule3))]
("Anne" "is" "big" "+")
triple1
((triple7) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not quiet.
False
1
inv-proof
[(triple5)]
("Anne" "is" "quiet" "-")
triple5
@0: Anne is big.[(triple1 OR ((triple7) -> rule3))] Anne is kind.[(triple3)] Anne is nice.[(triple4 OR ((triple7 triple2) -> rule1))] Anne is not cold.[(triple2)] Anne is quiet.[(triple5)] Anne is rough.[(triple6)] Anne is white.[(triple7)] Fiona is big.[(triple8)] Fiona is cold.[(triple9)] Fiona is kind.[(triple10 OR ((triple9) -> rule2))] Fiona is nice.[(triple11)] Fiona is not quiet.[(triple12)] Fiona is not rough.[(triple13)] Fiona is not white.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple7) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple7 triple2) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not cold.
("Anne" "is" "cold" "-")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
((triple9) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple12
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple13
Fiona is not white.
("Fiona" "is" "white" "-")
triple14