Anne is cold. Anne is not green. Anne is nice. Anne is rough. Anne is round. Anne is white. Anne is young. If Anne is nice and Anne is young then Anne is round. Young people are white. If someone is cold and not young then they are round.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not green.
("Anne" "is" "green" "-")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
If Anne is nice and Anne is young then Anne is round.
((("Anne" "is" "nice" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "round" "+"))
Young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is cold and not young then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "round" "+"))
Anne is young.
True
1
proof
[(triple7)]
("Anne" "is" "young" "+")
triple7
Anne is not round.
False
1
inv-proof
[(triple5 OR ((triple3 triple7) -> rule1))]
("Anne" "is" "round" "-")
triple5
((triple3 triple7) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
@0: Anne is cold.[(triple1)] Anne is nice.[(triple3)] Anne is not green.[(triple2)] Anne is rough.[(triple4)] Anne is round.[(triple5 OR ((triple3 triple7) -> rule1))] Anne is white.[(triple6 OR ((triple7) -> rule2))] Anne is young.[(triple7)]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is not green.
("Anne" "is" "green" "-")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple3 triple7) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple7) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple7