Anne is big. Anne is cold. Anne is nice. Anne is red. Anne is rough. Anne is white. Anne is young. If something is white then it is nice. White things are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Anne is nice.
True
1
proof
[(triple3 OR ((triple6) -> rule1))]
("Anne" "is" "nice" "+")
triple3
((triple6) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not red.
False
1
inv-proof
[(triple4)]
("Anne" "is" "red" "-")
triple4
@0: Anne is big.[(triple1 OR ((triple6) -> rule2))] Anne is cold.[(triple2)] Anne is nice.[(triple3 OR ((triple6) -> rule1))] Anne is red.[(triple4)] Anne is rough.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7)]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple6) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple6) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7