Anne is blue. Anne is cold. Anne is kind. Anne is nice. Anne is quiet. Anne is not white. Anne is young. Dave is not blue. Dave is cold. Dave is kind. Dave is nice. Dave is quiet. Dave is white. Dave is young. Young people are nice. Kind, blue people are quiet. If someone is cold and young then they are quiet. Blue, white people are quiet. If Anne is cold then Anne is not white. If Anne is kind then Anne is quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not white.
("Anne" "is" "white" "-")
Anne is young.
("Anne" "is" "young" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Kind, blue people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold and young then they are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Blue, white people are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is cold then Anne is not white.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "white" "-"))
If Anne is kind then Anne is quiet.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "quiet" "+"))
Dave is quiet.
True
1
proof
[(triple12 OR ((triple9 triple14) -> rule3))]
("Dave" "is" "quiet" "+")
triple12
((triple9 triple14) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not nice.
False
1
inv-proof
[(triple11 OR ((triple14) -> rule1))]
("Dave" "is" "nice" "-")
triple11
((triple14) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is kind.[(triple3)] Anne is nice.[(triple4 OR ((triple7) -> rule1))] Anne is not white.[(triple6 OR ((triple2) -> rule5))] Anne is quiet.[(triple5 OR ((triple3) -> rule6) OR ((triple2 triple7) -> rule3) OR ((triple3 triple1) -> rule2))] Anne is young.[(triple7)] Dave is cold.[(triple9)] Dave is kind.[(triple10)] Dave is nice.[(triple11 OR ((triple14) -> rule1))] Dave is not blue.[(triple8)] Dave is quiet.[(triple12 OR ((triple9 triple14) -> rule3))] Dave is white.[(triple13)] Dave is young.[(triple14)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple7) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
triple6
((triple2) -> (rule5 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
((triple3) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple2 triple7) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple3 triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
((triple14) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple12
((triple9 triple14) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple13
Dave is young.
("Dave" "is" "young" "+")
triple14