Dave is blue. Dave is not green. Dave is nice. Dave is smart. Dave is white. Dave is young. Erin is blue. Erin is green. Erin is rough. Erin is smart. Erin is white. Erin is young. White things are smart. All green things are blue. If something is white and not green then it is not rough.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
White things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is white and not green then it is not rough.
((("something" "is" "white" "+") ("something" "is" "green" "~")) -> ("something" "is" "rough" "-"))
Erin is young.
True
1
proof
[(triple12)]
("Erin" "is" "young" "+")
triple12
Dave is green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Dave is not rough.
True
3
proof
[(((triple5 triple2) -> rule3))]
("Dave" "is" "rough" "-")
((triple5 triple2) -> (rule3 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is rough.
False
3
inv-proof
[(((triple5 triple2) -> rule3))]
("Dave" "is" "rough" "+")
((triple5 triple2) -> (rule3 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
@0: Dave is blue.[(triple1)] Dave is nice.[(triple3)] Dave is not green.[(triple2)] Dave is smart.[(triple4 OR ((triple5) -> rule1))] Dave is white.[(triple5)] Dave is young.[(triple6)] Erin is blue.[(triple7 OR ((triple8) -> rule2))] Erin is green.[(triple8)] Erin is rough.[(triple9)] Erin is smart.[(triple10 OR ((triple11) -> rule1))] Erin is white.[(triple11)] Erin is young.[(triple12)] @1: Dave is not rough.[(((triple5 triple2) -> rule3))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is not green.
("Dave" "is" "green" "-")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple4
((triple5) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
((triple8) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
((triple11) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Dave is not rough.
("Dave" "is" "rough" "-")
((triple5 triple2) -> (rule3 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1