Anne is big. Anne is furry. Anne is nice. Anne is quiet. Anne is red. Anne is round. Anne is white. All round, big things are quiet. If something is furry then it is round. If something is red and big then it is round. If something is quiet then it is furry. White, red things are furry. Round, nice things are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
All round, big things are quiet.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is furry then it is round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If something is red and big then it is round.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
White, red things are furry.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Round, nice things are white.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
@0: Anne is big.[(triple1)] Anne is furry.[(triple2 OR ((triple4) -> rule4) OR ((triple7 triple5) -> rule5) OR ((((triple6 triple1) -> rule1)) -> rule4) OR ((((triple6 triple3) -> rule6) triple5) -> rule5) OR ((((((triple5 triple1) -> rule3) triple1) -> rule1)) -> rule4) OR ((((((triple5 triple1) -> rule3) triple3) -> rule6) triple5) -> rule5))] Anne is nice.[(triple3)] Anne is quiet.[(triple4 OR ((triple6 triple1) -> rule1) OR ((((triple2) -> rule2) triple1) -> rule1) OR ((((triple5 triple1) -> rule3) triple1) -> rule1) OR ((((((triple7 triple5) -> rule5)) -> rule2) triple1) -> rule1))] Anne is red.[(triple5)] Anne is round.[(triple6 OR ((triple2) -> rule2) OR ((triple5 triple1) -> rule3) OR ((((triple4) -> rule4)) -> rule2) OR ((((triple7 triple5) -> rule5)) -> rule2))] Anne is white.[(triple7 OR ((triple6 triple3) -> rule6) OR ((((triple2) -> rule2) triple3) -> rule6) OR ((((triple5 triple1) -> rule3) triple3) -> rule6) OR ((((((triple4) -> rule4)) -> rule2) triple3) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple4) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple7 triple5) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple6 triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple6 triple3) -> (rule6 % int2)) triple5) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple5 triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((triple5 triple1) -> (rule3 % int3)) triple3) -> (rule6 % int2)) triple5) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple6 triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple2) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple5 triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((((triple7 triple5) -> (rule5 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple5 triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple7 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple6 triple3) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple2) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple5 triple1) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3