Anne is big. Anne is furry. Anne is quiet. Anne is rough. Anne is round. Anne is smart. Anne is white. If someone is white then they are furry. If someone is smart then they are round. If someone is furry and quiet then they are white. If someone is smart and rough then they are big. If someone is quiet then they are white. If Anne is furry and Anne is big then Anne is smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
If someone is white then they are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is furry and quiet then they are white.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is smart and rough then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If Anne is furry and Anne is big then Anne is smart.
((("Anne" "is" "furry" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "smart" "+"))
Anne is quiet.
True
1
proof
[(triple3)]
("Anne" "is" "quiet" "+")
triple3
Anne is not smart.
False
1
inv-proof
[(triple6 OR ((triple2 triple1) -> rule6) OR ((((triple7) -> rule1) triple1) -> rule6) OR ((((((triple3) -> rule5)) -> rule1) triple1) -> rule6))]
("Anne" "is" "smart" "-")
triple6
((triple2 triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple7) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
@0: Anne is big.[(triple1 OR ((triple6 triple4) -> rule4))] Anne is furry.[(triple2 OR ((triple7) -> rule1) OR ((((triple3) -> rule5)) -> rule1))] Anne is quiet.[(triple3)] Anne is rough.[(triple4)] Anne is round.[(triple5 OR ((triple6) -> rule2) OR ((((triple2 triple1) -> rule6)) -> rule2) OR ((((((triple7) -> rule1) triple1) -> rule6)) -> rule2) OR ((((((((triple3) -> rule5)) -> rule1) triple1) -> rule6)) -> rule2))] Anne is smart.[(triple6 OR ((triple2 triple1) -> rule6) OR ((((triple7) -> rule1) triple1) -> rule6) OR ((((((triple3) -> rule5)) -> rule1) triple1) -> rule6))] Anne is white.[(triple7 OR ((triple3) -> rule5) OR ((triple2 triple3) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple6 triple4) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple7) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple6) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2 triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((((triple7) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((((((triple3) -> (rule5 % int4))) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple2 triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple7) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple3) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple2 triple3) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1