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