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