Dave is big. Dave is green. Dave is kind. Dave is rough. Dave is round. Dave is white. Dave is young. Erin is big. Erin is green. Erin is rough. Erin is round. Erin is young. If someone is rough then they are kind. Young, kind people are white.
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is rough then they are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Young, kind people are white.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not white.
False
1
inv-proof
[(triple6 OR ((triple7 triple3) -> rule2) OR ((triple7 ((triple4) -> rule1)) -> rule2))]
("Dave" "is" "white" "-")
triple6
((triple7 triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple7 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is kind.
True
2
proof
[(((triple10) -> rule1))]
("Erin" "is" "kind" "+")
((triple10) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple10) -> rule1))]
("Erin" "is" "kind" "-")
((triple10) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
True
4
proof
[(((triple12 ((triple10) -> rule1)) -> rule2))]
("Erin" "is" "white" "+")
((triple12 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not white.
False
4
inv-proof
[(((triple12 ((triple10) -> rule1)) -> rule2))]
("Erin" "is" "white" "-")
((triple12 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
@0: Dave is big.[(triple1)] Dave is green.[(triple2)] Dave is kind.[(triple3 OR ((triple4) -> rule1))] Dave is rough.[(triple4)] Dave is round.[(triple5)] Dave is white.[(triple6 OR ((triple7 triple3) -> rule2) OR ((triple7 ((triple4) -> rule1)) -> rule2))] Dave is young.[(triple7)] Erin is big.[(triple8)] Erin is green.[(triple9)] Erin is rough.[(triple10)] Erin is round.[(triple11)] Erin is young.[(triple12)] @1: Erin is kind.[(((triple10) -> rule1))] @2: Erin is white.[(((triple12 ((triple10) -> rule1)) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple4) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple7 triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple7 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Erin is kind.
("Erin" "is" "kind" "+")
((triple10) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple12 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2