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