Anne is furry. Anne is green. Anne is quiet. Anne is red. Anne is round. Anne is smart. Anne is young. Bob is furry. Bob is green. Bob is quiet. Bob is red. Bob is round. Bob is smart. Bob is young. All quiet, red people are young. If someone is quiet then they are young. If Anne is red then Anne is quiet. If someone is quiet and not young then they are not round. If someone is green and not young then they are furry. If Bob is furry and Bob is not green then Bob is not smart.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
All quiet, red people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If Anne is red then Anne is quiet.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "quiet" "+"))
If someone is quiet and not young then they are not round.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "round" "-"))
If someone is green and not young then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "furry" "+"))
If Bob is furry and Bob is not green then Bob is not smart.
((("Bob" "is" "furry" "+") ("Bob" "is" "green" "~")) -> ("Bob" "is" "smart" "-"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not red.
False
1
inv-proof
[(triple4)]
("Anne" "is" "red" "-")
triple4
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Anne is quiet.[(triple3 OR ((triple4) -> rule3))] Anne is red.[(triple4)] Anne is round.[(triple5)] Anne is smart.[(triple6)] Anne is young.[(triple7 OR ((triple3) -> rule2) OR ((triple3 triple4) -> rule1) OR ((((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule3) triple4) -> rule1))] Bob is furry.[(triple8)] Bob is green.[(triple9)] Bob is quiet.[(triple10)] Bob is red.[(triple11)] Bob is round.[(triple12)] Bob is smart.[(triple13)] Bob is young.[(triple14 OR ((triple10) -> rule2) OR ((triple10 triple11) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple4) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple3) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple3 triple4) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple4) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple8
Bob is green.
("Bob" "is" "green" "+")
triple9
Bob is quiet.
("Bob" "is" "quiet" "+")
triple10
Bob is red.
("Bob" "is" "red" "+")
triple11
Bob is round.
("Bob" "is" "round" "+")
triple12
Bob is smart.
("Bob" "is" "smart" "+")
triple13
Bob is young.
("Bob" "is" "young" "+")
triple14
((triple10) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple10 triple11) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1