Anne is not blue. Anne is cold. Anne is kind. Anne is quiet. Anne is round. Anne is white. Anne is young. If something is young and kind then it is white. If something is white and young then it is round.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
If something is young and kind then it is white.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is white and young then it is round.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Anne is young.
True
1
proof
[(triple7)]
("Anne" "is" "young" "+")
triple7
Anne is not white.
False
1
inv-proof
[(triple6 OR ((triple7 triple3) -> rule1))]
("Anne" "is" "white" "-")
triple6
((triple7 triple3) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
@0: Anne is cold.[(triple2)] Anne is kind.[(triple3)] Anne is not blue.[(triple1)] Anne is quiet.[(triple4)] Anne is round.[(triple5 OR ((triple6 triple7) -> rule2) OR ((((triple7 triple3) -> rule1) triple7) -> rule2))] Anne is white.[(triple6 OR ((triple7 triple3) -> rule1))] Anne is young.[(triple7)]
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple6 triple7) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple7 triple3) -> (rule1 % int2)) triple7) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple7 triple3) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple7