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