Dave is big. Dave is furry. Dave is kind. Dave is nice. Erin is big. Erin is blue. Erin is furry. Nice people are blue. All white, kind people are big. Big people are white. White people are blue. All kind, white people are young. Furry, white people are kind.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
All white, kind people are big.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
White people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
All kind, white people are young.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
Furry, white people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Erin is furry.
True
1
proof
[(triple7)]
("Erin" "is" "furry" "+")
triple7
Dave is not kind.
False
1
inv-proof
[(triple3 OR ((triple2 ((triple1) -> rule3)) -> rule6))]
("Dave" "is" "kind" "-")
triple3
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Erin is white.
True
2
proof
[(((triple5) -> rule3))]
("Erin" "is" "white" "+")
((triple5) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "white" "-")
((triple1) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
True
4
proof
[(((triple3 ((triple1) -> rule3)) -> rule5) OR ((((triple2 ((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule5))]
("Dave" "is" "young" "+")
((triple3 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2 ((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Erin is not kind.
False
4
inv-proof
[(((triple7 ((triple5) -> rule3)) -> rule6))]
("Erin" "is" "kind" "-")
((triple7 ((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
True
7
proof
[(((((triple7 ((triple5) -> rule3)) -> rule6) ((triple5) -> rule3)) -> rule5))]
("Erin" "is" "young" "+")
((((triple7 ((triple5) -> (rule3 % int3))) -> (rule6 % int2)) ((triple5) -> (rule3 % int3))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is not young.
False
7
inv-proof
[(((((triple7 ((triple5) -> rule3)) -> rule6) ((triple5) -> rule3)) -> rule5))]
("Erin" "is" "young" "-")
((((triple7 ((triple5) -> (rule3 % int3))) -> (rule6 % int2)) ((triple5) -> (rule3 % int3))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
@0: Dave is big.[(triple1)] Dave is furry.[(triple2)] Dave is kind.[(triple3 OR ((triple2 ((triple1) -> rule3)) -> rule6))] Dave is nice.[(triple4)] Erin is big.[(triple5)] Erin is blue.[(triple6 OR ((((triple5) -> rule3)) -> rule4))] Erin is furry.[(triple7)] @1: Dave is blue.[(((triple4) -> rule1) OR ((((triple1) -> rule3)) -> rule4))] Dave is white.[(((triple1) -> rule3))] Erin is white.[(((triple5) -> rule3))] @2: Dave is young.[(((triple3 ((triple1) -> rule3)) -> rule5) OR ((((triple2 ((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule5))] Erin is kind.[(((triple7 ((triple5) -> rule3)) -> rule6))] @3: Erin is young.[(((((triple7 ((triple5) -> rule3)) -> rule6) ((triple5) -> rule3)) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple5) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2 ((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((triple7 ((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple7 ((triple5) -> (rule3 % int3))) -> (rule6 % int2)) ((triple5) -> (rule3 % int3))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3