Anne is blue. Anne is cold. Anne is furry. Anne is green. Anne is nice. Anne is red. Anne is white. Dave is blue. Dave is not cold. Dave is furry. Dave is green. Dave is nice. Dave is not red. Dave is not white. If Anne is blue and Anne is nice then Anne is furry. If someone is white and not blue then they are red. White people are nice. If someone is furry and not red then they are green. All green people are furry. If someone is red then they are furry. If someone is blue and not white then they are furry. All red people are furry.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not white.
("Dave" "is" "white" "-")
If Anne is blue and Anne is nice then Anne is furry.
((("Anne" "is" "blue" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "furry" "+"))
If someone is white and not blue then they are red.
((("someone" "is" "white" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "red" "+"))
White people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry and not red then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "green" "+"))
All green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If someone is red then they are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If someone is blue and not white then they are furry.
((("someone" "is" "blue" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "furry" "+"))
All red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Dave is not cold.
True
1
proof
[(triple9)]
("Dave" "is" "cold" "-")
triple9
Dave is not blue.
False
1
inv-proof
[(triple8)]
("Dave" "is" "blue" "-")
triple8
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is furry.[(triple3 OR ((triple4) -> rule5) OR ((triple6) -> rule6) OR ((triple6) -> rule8) OR ((triple1 triple5) -> rule1) OR ((triple1 ((triple7) -> rule3)) -> rule1))] Anne is green.[(triple4)] Anne is nice.[(triple5 OR ((triple7) -> rule3))] Anne is red.[(triple6)] Anne is white.[(triple7)] Dave is blue.[(triple8)] Dave is furry.[(triple10 OR ((triple11) -> rule5) OR ((triple8 triple14) -> rule7))] Dave is green.[(triple11 OR ((triple10 triple13) -> rule4) OR ((((triple8 triple14) -> rule7) triple13) -> rule4))] Dave is nice.[(triple12)] Dave is not cold.[(triple9)] Dave is not red.[(triple13)] Dave is not white.[(triple14)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple4) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple6) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple6) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple1 triple5) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple1 ((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
triple5
((triple7) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple10
((triple11) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple8 triple14) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple11
((triple10 triple13) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple8 triple14) -> (rule7 % int2)) triple13) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple12
Dave is not cold.
("Dave" "is" "cold" "-")
triple9
Dave is not red.
("Dave" "is" "red" "-")
triple13
Dave is not white.
("Dave" "is" "white" "-")
triple14