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