Anne is big. Anne is furry. Anne is nice. Anne is white. Anne is not young. Charlie is big. Charlie is blue. Charlie is furry. Charlie is green. Charlie is nice. Charlie is white. Charlie is young. Dave is blue. Dave is furry. Dave is white. Dave is young. White, big people are green. Nice people are green. Blue people are white. All blue people are big. Young people are nice. If Charlie is young then Charlie is furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is not young.
("Anne" "is" "young" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
White, big people are green.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is young then Charlie is furry.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "furry" "+"))
Charlie is nice.
True
1
proof
[(triple10 OR ((triple12) -> rule5))]
("Charlie" "is" "nice" "+")
triple10
((triple12) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not young.
False
1
inv-proof
[(triple12)]
("Charlie" "is" "young" "-")
triple12
Dave is big.
True
2
proof
[(((triple13) -> rule4))]
("Dave" "is" "big" "+")
((triple13) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple3) -> rule2) OR ((triple4 triple1) -> rule1))]
("Anne" "is" "green" "-")
((triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4 triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is green.
True
3
proof
[(((((triple16) -> rule5)) -> rule2) OR ((triple15 ((triple13) -> rule4)) -> rule1) OR ((((triple13) -> rule3) ((triple13) -> rule4)) -> rule1))]
("Dave" "is" "green" "+")
((((triple16) -> (rule5 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple15 ((triple13) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple13) -> (rule3 % int3)) ((triple13) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not green.
False
3
inv-proof
[(((((triple16) -> rule5)) -> rule2) OR ((triple15 ((triple13) -> rule4)) -> rule1) OR ((((triple13) -> rule3) ((triple13) -> rule4)) -> rule1))]
("Dave" "is" "green" "-")
((((triple16) -> (rule5 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple15 ((triple13) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple13) -> (rule3 % int3)) ((triple13) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is nice.[(triple3)] Anne is not young.[(triple5)] Anne is white.[(triple4)] Charlie is big.[(triple6 OR ((triple7) -> rule4))] Charlie is blue.[(triple7)] Charlie is furry.[(triple8 OR ((triple12) -> rule6))] Charlie is green.[(triple9 OR ((triple10) -> rule2) OR ((triple11 triple6) -> rule1) OR ((((triple12) -> rule5)) -> rule2) OR ((triple11 ((triple7) -> rule4)) -> rule1) OR ((((triple7) -> rule3) triple6) -> rule1) OR ((((triple7) -> rule3) ((triple7) -> rule4)) -> rule1))] Charlie is nice.[(triple10 OR ((triple12) -> rule5))] Charlie is white.[(triple11 OR ((triple7) -> rule3))] Charlie is young.[(triple12)] Dave is blue.[(triple13)] Dave is furry.[(triple14)] Dave is white.[(triple15 OR ((triple13) -> rule3))] Dave is young.[(triple16)] @1: Anne is green.[(((triple3) -> rule2) OR ((triple4 triple1) -> rule1))] Dave is big.[(((triple13) -> rule4))] Dave is nice.[(((triple16) -> rule5))] @2: Dave is green.[(((((triple16) -> rule5)) -> rule2) OR ((triple15 ((triple13) -> rule4)) -> rule1) OR ((((triple13) -> rule3) ((triple13) -> rule4)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is not young.
("Anne" "is" "young" "-")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple6
((triple7) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
((triple12) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple9
((triple10) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple11 triple6) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((triple11 ((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple7) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple7) -> (rule3 % int3)) ((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple10
((triple12) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple11
((triple7) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple12
Dave is blue.
("Dave" "is" "blue" "+")
triple13
Dave is furry.
("Dave" "is" "furry" "+")
triple14
Dave is white.
("Dave" "is" "white" "+")
triple15
((triple13) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple16
Anne is green.
("Anne" "is" "green" "+")
((triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4 triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple13) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple16) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple16) -> (rule5 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple15 ((triple13) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple13) -> (rule3 % int3)) ((triple13) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3