Anne is furry. Anne is kind. Anne is rough. Anne is smart. Anne is young. Dave is furry. Dave is kind. Dave is quiet. Dave is red. Dave is rough. Dave is smart. Dave is young. If Anne is quiet and Anne is rough then Anne is young. If someone is red then they are quiet. If someone is young and smart then they are furry. If someone is furry then they are quiet. If Dave is smart then Dave is rough. Furry, kind people are smart. All quiet people are red. All quiet, furry people are young.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
If Anne is quiet and Anne is rough then Anne is young.
((("Anne" "is" "quiet" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "young" "+"))
If someone is red then they are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young and smart then they are furry.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is smart then Dave is rough.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "rough" "+"))
Furry, kind people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
All quiet, furry people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Dave is furry.
True
1
proof
[(triple6 OR ((triple12 triple11) -> rule3))]
("Dave" "is" "furry" "+")
triple6
((triple12 triple11) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Anne is not young.
False
1
inv-proof
[(triple5 OR ((((triple1) -> rule4) triple1) -> rule8) OR ((((triple1) -> rule4) triple3) -> rule1))]
("Anne" "is" "young" "-")
triple5
((((triple1) -> (rule4 % int2)) triple1) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple1) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is quiet.
True
2
proof
[(((triple1) -> rule4) OR ((((triple5 triple4) -> rule3)) -> rule4))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple5 triple4) -> (rule3 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule4) OR ((((triple5 triple4) -> rule3)) -> rule4))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple5 triple4) -> (rule3 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
True
3
proof
[(((((triple1) -> rule4)) -> rule7) OR ((((((triple5 triple4) -> rule3)) -> rule4)) -> rule7))]
("Anne" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple5 triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7) OR ((((((triple5 triple4) -> rule3)) -> rule4)) -> rule7))]
("Anne" "is" "red" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple5 triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
@0: Anne is furry.[(triple1 OR ((triple5 triple4) -> rule3))] Anne is kind.[(triple2)] Anne is rough.[(triple3)] Anne is smart.[(triple4 OR ((triple1 triple2) -> rule6))] Anne is young.[(triple5 OR ((((triple1) -> rule4) triple1) -> rule8) OR ((((triple1) -> rule4) triple3) -> rule1))] Dave is furry.[(triple6 OR ((triple12 triple11) -> rule3))] Dave is kind.[(triple7)] Dave is quiet.[(triple8 OR ((triple6) -> rule4) OR ((triple9) -> rule2) OR ((((triple12 triple11) -> rule3)) -> rule4))] Dave is red.[(triple9 OR ((triple8) -> rule7) OR ((((triple6) -> rule4)) -> rule7) OR ((((((triple12 triple11) -> rule3)) -> rule4)) -> rule7))] Dave is rough.[(triple10 OR ((triple11) -> rule5) OR ((((triple6 triple7) -> rule6)) -> rule5))] Dave is smart.[(triple11 OR ((triple6 triple7) -> rule6))] Dave is young.[(triple12 OR ((triple8 triple6) -> rule8) OR ((((triple6) -> rule4) triple6) -> rule8) OR ((((triple9) -> rule2) triple6) -> rule8))] @1: Anne is quiet.[(((triple1) -> rule4) OR ((((triple5 triple4) -> rule3)) -> rule4))] @2: Anne is red.[(((((triple1) -> rule4)) -> rule7) OR ((((((triple5 triple4) -> rule3)) -> rule4)) -> rule7))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple5 triple4) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((triple1 triple2) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple5
((((triple1) -> (rule4 % int2)) triple1) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple1) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple6
((triple12 triple11) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple6) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple9) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple12 triple11) -> (rule3 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple8) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple6) -> (rule4 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((((triple12 triple11) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
triple10
((triple11) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple6 triple7) -> (rule6 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple11
((triple6 triple7) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple12
((triple8 triple6) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple6) -> (rule4 % int2)) triple6) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple9) -> (rule2 % int2)) triple6) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple5 triple4) -> (rule3 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple5 triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3