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