Dave is kind. Dave is not quiet. Dave is red. Dave is rough. Dave is round. Dave is white. Erin is furry. Erin is kind. Erin is quiet. Erin is red. Erin is rough. Erin is white. All kind people are furry. All white people are rough. If Dave is kind and Dave is round then Dave is furry.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
All kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
All white people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If Dave is kind and Dave is round then Dave is furry.
((("Dave" "is" "kind" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "furry" "+"))
Erin is furry.
True
1
proof
[(triple7 OR ((triple8) -> rule1))]
("Erin" "is" "furry" "+")
triple7
((triple8) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Dave is quiet.
False
1
inv-proof
[(triple2)]
("Dave" "is" "quiet" "+")
triple2
Dave is furry.
True
2
proof
[(((triple1) -> rule1) OR ((triple1 triple5) -> rule3))]
("Dave" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple1 triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1 triple5) -> rule3))]
("Dave" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple1 triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
@0: Dave is kind.[(triple1)] Dave is not quiet.[(triple2)] Dave is red.[(triple3)] Dave is rough.[(triple4 OR ((triple6) -> rule2))] Dave is round.[(triple5)] Dave is white.[(triple6)] Erin is furry.[(triple7 OR ((triple8) -> rule1))] Erin is kind.[(triple8)] Erin is quiet.[(triple9)] Erin is red.[(triple10)] Erin is rough.[(triple11 OR ((triple12) -> rule2))] Erin is white.[(triple12)] @1: Dave is furry.[(((triple1) -> rule1) OR ((triple1 triple5) -> rule3))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
((triple6) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
((triple8) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple10
Erin is rough.
("Erin" "is" "rough" "+")
triple11
((triple12) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple12
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple1 triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1