Anne is big. Anne is blue. Anne is furry. Anne is green. Anne is nice. Anne is quiet. Anne is young. Charlie is blue. Charlie is furry. Charlie is green. Charlie is nice. Charlie is quiet. All green people are big. All big people are green. All green people are quiet. All big, furry people are green. If Charlie is big and Charlie is young then Charlie is blue. If Charlie is quiet then Charlie is furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
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 quiet.
("Charlie" "is" "quiet" "+")
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
All big, furry people are green.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If Charlie is big and Charlie is young then Charlie is blue.
((("Charlie" "is" "big" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "blue" "+"))
If Charlie is quiet then Charlie is furry.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "furry" "+"))
Anne is quiet.
True
1
proof
[(triple6 OR ((triple4) -> rule3) OR ((((triple1) -> rule2)) -> rule3) OR ((((triple1 triple3) -> rule4)) -> rule3))]
("Anne" "is" "quiet" "+")
triple6
((triple4) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple1 triple3) -> (rule4 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not green.
False
1
inv-proof
[(triple4 OR ((triple1) -> rule2) OR ((triple1 triple3) -> rule4))]
("Anne" "is" "green" "-")
triple4
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple1 triple3) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is big.
True
2
proof
[(((triple10) -> rule1))]
("Charlie" "is" "big" "+")
((triple10) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple10) -> rule1))]
("Charlie" "is" "big" "-")
((triple10) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
@0: Anne is big.[(triple1 OR ((triple4) -> rule1))] Anne is blue.[(triple2)] Anne is furry.[(triple3)] Anne is green.[(triple4 OR ((triple1) -> rule2) OR ((triple1 triple3) -> rule4))] Anne is nice.[(triple5)] Anne is quiet.[(triple6 OR ((triple4) -> rule3) OR ((((triple1) -> rule2)) -> rule3) OR ((((triple1 triple3) -> rule4)) -> rule3))] Anne is young.[(triple7)] Charlie is blue.[(triple8)] Charlie is furry.[(triple9 OR ((triple12) -> rule6) OR ((((triple10) -> rule3)) -> rule6))] Charlie is green.[(triple10)] Charlie is nice.[(triple11)] Charlie is quiet.[(triple12 OR ((triple10) -> rule3))] @1: Charlie is big.[(((triple10) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
triple4
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple1 triple3) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Anne is quiet.
("Anne" "is" "quiet" "+")
triple6
((triple4) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple1 triple3) -> (rule4 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
((triple12) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
triple11
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple12
((triple10) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple10) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1