Anne is nice. Big people are quiet. If Anne is furry then Anne is smart. If Anne is quiet then Anne is round. If someone is big then they are furry. If Anne is nice then Anne is big. All nice people are young. All round people are young. Quiet people are big.
Anne is nice.
("Anne" "is" "nice" "+")
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is furry then Anne is smart.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "smart" "+"))
If Anne is quiet then Anne is round.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "round" "+"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If Anne is nice then Anne is big.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "big" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Anne is young.
True
2
proof
[(((triple1) -> rule6) OR ((((((((triple1) -> rule5)) -> rule1)) -> rule3)) -> rule7))]
("Anne" "is" "young" "+")
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "big" "-")
((triple1) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
True
4
proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule2))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not smart.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule2))]
("Anne" "is" "smart" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
@0: Anne is nice.[(triple1)] @1: Anne is big.[(((triple1) -> rule5))] Anne is young.[(((triple1) -> rule6) OR ((((((((triple1) -> rule5)) -> rule1)) -> rule3)) -> rule7))] @2: Anne is furry.[(((((triple1) -> rule5)) -> rule4))] Anne is quiet.[(((((triple1) -> rule5)) -> rule1))] @3: Anne is round.[(((((((triple1) -> rule5)) -> rule1)) -> rule3))] Anne is smart.[(((((((triple1) -> rule5)) -> rule4)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3