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