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